Skip to content

Commit e00a6b9

Browse files
Add missing proof_for_contract to mut_ptr::offset_from harness (#358)
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Michael Tautschnig <[email protected]>
1 parent 81b5eea commit e00a6b9

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

library/core/src/ptr/mut_ptr.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2613,6 +2613,7 @@ mod verify {
26132613
}
26142614

26152615
// Below function is for large arrays
2616+
#[kani::proof_for_contract(<*mut $type>::offset_from)]
26162617
pub fn $proof_name2() {
26172618
const gen_size: usize = mem::size_of::<$type>();
26182619
let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();

0 commit comments

Comments
 (0)