@@ -2430,32 +2430,6 @@ mod verify {
24302430 nonzero_check ! ( u128 , core:: num:: NonZeroU128 , nonzero_check_new_unchecked_for_u128) ;
24312431 nonzero_check ! ( usize , core:: num:: NonZeroUsize , nonzero_check_new_unchecked_for_usize) ;
24322432
2433- // macro_rules! nonzero_check_from_mut_unchecked {
2434- // ($t:ty, $nonzero_type:ty, $harness_name:ident) => {
2435- // #[kani::proof_for_contract(<T>::from_mut_unchecked)]
2436- // pub fn $harness_name() {
2437- // let mut x: $t = kani::any();
2438- // unsafe {
2439- // <$nonzero_type>::from_mut_unchecked(&mut x);
2440- // }
2441- // }
2442- // };
2443- // }
2444-
2445- // // Generate harnesses for multiple types
2446- // nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8);
2447- // nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16);
2448- // nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32);
2449- // nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64);
2450- // nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128);
2451- // nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize);
2452- // nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8);
2453- // nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16);
2454- // nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32);
2455- // nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64);
2456- // nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128);
2457- // nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize);
2458-
24592433 macro_rules! nonzero_check_cmp {
24602434 ( $nonzero_type: ty, $nonzero_check_cmp_for: ident) => {
24612435 #[ kani:: proof]
0 commit comments