Skip to content

Commit

Permalink
Revert "Try to use Arbitrary"
Browse files Browse the repository at this point in the history
This reverts commit 16f40c7.
  • Loading branch information
tautschnig committed Aug 16, 2024
1 parent 16f40c7 commit 729fbc0
Showing 1 changed file with 4 additions and 9 deletions.
13 changes: 4 additions & 9 deletions library/core/src/ptr/alignment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -388,13 +388,6 @@ enum AlignmentEnum {
mod verify {
use super::*;

impl kani::Arbitrary for Alignment {
fn any() -> Self {
let align = kani::any_where(|a: &usize| a.is_power_of_two());
unsafe { mem::transmute::<usize, Alignment>(align) }
}
}

// pub const fn of<T>() -> Self
#[kani::proof]
pub fn check_of_i32() {
Expand Down Expand Up @@ -430,8 +423,10 @@ mod verify {
// pub const fn as_nonzero(self) -> NonZero<usize>
#[kani::proof_for_contract(Alignment::as_nonzero)]
pub fn check_as_nonzero() {
let alignment = kani::any::<Alignment>();
let _ = alignment.as_nonzero();
let a = kani::any::<usize>();
if let Some(alignment) = Alignment::new(a) {
let _ = alignment.as_nonzero();
}
}

// pub const fn log2(self) -> u32
Expand Down

0 comments on commit 729fbc0

Please sign in to comment.