Skip to content

Commit 6dbf58e

Browse files
committed
Apply suggestions
1 parent 1e5ba53 commit 6dbf58e

File tree

1 file changed

+2
-9
lines changed

1 file changed

+2
-9
lines changed

library/core/src/alloc/layout.rs

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -121,9 +121,7 @@ impl Layout {
121121
#[must_use]
122122
#[inline]
123123
#[rustc_allow_const_fn_unstable(ptr_alignment_type)]
124-
#[requires(align > 0)]
125-
#[requires((align & (align - 1)) == 0)]
126-
#[requires(size <= isize::MAX as usize - (align - 1))]
124+
#[requires(Layout::from_size_align(size, align).is_ok())]
127125
pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
128126
// SAFETY: the caller is required to uphold the preconditions.
129127
unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -507,13 +505,8 @@ mod verify {
507505

508506
#[kani::proof_for_contract(Layout::from_size_align_unchecked)]
509507
pub fn check_from_size_align_unchecked() {
510-
let shift_index = kani::any::<usize>();
511-
kani::assume(shift_index < core::mem::size_of::<usize>() * 8);
512-
let a : usize = 1 << shift_index;
513-
kani::assume(a > 0);
514-
515508
let s = kani::any::<usize>();
516-
kani::assume(s <= isize::MAX as usize - (a - 1));
509+
let a = kani::any::<usize>();
517510

518511
unsafe {
519512
let layout = Layout::from_size_align_unchecked(s, a);

0 commit comments

Comments
 (0)