Skip to content

Commit 41f23a1

Browse files
committed
Fixes a bug in the unit type proofs
1 parent 5f2125c commit 41f23a1

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

library/core/src/ptr/const_ptr.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -2134,7 +2134,7 @@ mod verify {
21342134
pub fn $proof_name() {
21352135
let val = ();
21362136
let ptr: *const () = &val;
2137-
let count: isize = kani::any();
2137+
let count: isize = mem::size_of::<()>() as isize;
21382138
unsafe {
21392139
ptr.byte_offset(count);
21402140
}
@@ -2147,7 +2147,7 @@ mod verify {
21472147
let val = ();
21482148
let ptr: *const () = &val;
21492149
//byte_add and byte_sub need count to be usize unlike byte_offset
2150-
let count: usize = kani::any();
2150+
let count: usize = mem::size_of::<()>();
21512151
unsafe {
21522152
ptr.$fn_name(count);
21532153
}

0 commit comments

Comments
 (0)