Skip to content

Commit 729fbc0

Browse files
committed
Revert "Try to use Arbitrary"
This reverts commit 16f40c7.
1 parent 16f40c7 commit 729fbc0

File tree

1 file changed

+4
-9
lines changed

1 file changed

+4
-9
lines changed

library/core/src/ptr/alignment.rs

+4-9
Original file line numberDiff line numberDiff line change
@@ -388,13 +388,6 @@ enum AlignmentEnum {
388388
mod verify {
389389
use super::*;
390390

391-
impl kani::Arbitrary for Alignment {
392-
fn any() -> Self {
393-
let align = kani::any_where(|a: &usize| a.is_power_of_two());
394-
unsafe { mem::transmute::<usize, Alignment>(align) }
395-
}
396-
}
397-
398391
// pub const fn of<T>() -> Self
399392
#[kani::proof]
400393
pub fn check_of_i32() {
@@ -430,8 +423,10 @@ mod verify {
430423
// pub const fn as_nonzero(self) -> NonZero<usize>
431424
#[kani::proof_for_contract(Alignment::as_nonzero)]
432425
pub fn check_as_nonzero() {
433-
let alignment = kani::any::<Alignment>();
434-
let _ = alignment.as_nonzero();
426+
let a = kani::any::<usize>();
427+
if let Some(alignment) = Alignment::new(a) {
428+
let _ = alignment.as_nonzero();
429+
}
435430
}
436431

437432
// pub const fn log2(self) -> u32

0 commit comments

Comments
 (0)