Skip to content

Commit 2e9f3f6

Browse files
committed
Limit shift
1 parent 8ab7ec6 commit 2e9f3f6

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

library/core/src/alloc/layout.rs

+4-3
Original file line numberDiff line numberDiff line change
@@ -507,11 +507,12 @@ mod verify {
507507

508508
#[kani::proof_for_contract(Layout::from_size_align_unchecked)]
509509
pub fn check_from_size_align_unchecked() {
510-
let s = kani::any::<usize>();
511-
let shift_index = kani::any::<u8>();
510+
let shift_index = kani::any::<usize>();
511+
kani::assume(shift_index < core::mem::size_of::<usize>() * 8);
512512
let a : usize = 1 << shift_index;
513-
514513
kani::assume(a > 0);
514+
515+
let s = kani::any::<usize>();
515516
kani::assume(s <= isize::MAX as usize - (a - 1));
516517

517518
unsafe {

0 commit comments

Comments
 (0)