Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Limit shift
Browse files Browse the repository at this point in the history
tautschnig committed Jul 10, 2024
1 parent 8ab7ec6 commit 2e9f3f6
Showing 1 changed file with 4 additions and 3 deletions.
7 changes: 4 additions & 3 deletions library/core/src/alloc/layout.rs
Original file line number Diff line number Diff line change
@@ -507,11 +507,12 @@ mod verify {

#[kani::proof_for_contract(Layout::from_size_align_unchecked)]
pub fn check_from_size_align_unchecked() {
let s = kani::any::<usize>();
let shift_index = kani::any::<u8>();
let shift_index = kani::any::<usize>();
kani::assume(shift_index < core::mem::size_of::<usize>() * 8);
let a : usize = 1 << shift_index;

kani::assume(a > 0);

let s = kani::any::<usize>();
kani::assume(s <= isize::MAX as usize - (a - 1));

unsafe {

0 comments on commit 2e9f3f6

Please sign in to comment.