Skip to content

Commit

Permalink
Revert "Also drop unit test of our stub that uses ToBitMask"
Browse files Browse the repository at this point in the history
This reverts commit ba6b95e.
  • Loading branch information
tautschnig committed Dec 4, 2023
1 parent ba6b95e commit cdf13e8
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions library/kani/src/models/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -184,6 +184,20 @@ mod test {
check_bitmask::<_, [u8; 9], i128, 70>(CustomMask([-1i128; 70]));
}

/// Compare the value returned by our model and the portable simd representation.
fn check_portable_bitmask<T, E, const LANES: usize>(mask: T)
where
T: ToBitMask + Clone,
T::BitMask: Debug + PartialEq,
E: kani_intrinsic::MaskElement,
[u8; kani_intrinsic::mask_len(LANES)]: Sized,
{
assert_eq!(
unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) },
mask.to_bitmask()
);
}

/// Compare the value returned by our model and the simd_bitmask intrinsic.
fn check_bitmask<T, U, E, const LANES: usize>(mask: T)
where
Expand Down

0 comments on commit cdf13e8

Please sign in to comment.