@@ -452,13 +452,6 @@ where
452
452
#[ unstable( feature = "nonzero_from_mut" , issue = "106290" ) ]
453
453
#[ must_use]
454
454
#[ inline]
455
- // TODO: not sure how to refer to a parameter that is a mutable reference
456
- // #[requires({
457
- // let size = core::mem::size_of::<T>();
458
- // let ptr = n as *const T as *const u8;
459
- // let slice = unsafe { core::slice::from_raw_parts(ptr, size) };
460
- // !slice.iter().all(|&byte| byte == 0)
461
- // })]
462
455
pub unsafe fn from_mut_unchecked ( n : & mut T ) -> & mut Self {
463
456
match Self :: from_mut ( n) {
464
457
Some ( n) => n,
@@ -2435,32 +2428,6 @@ mod verify {
2435
2428
nonzero_check ! ( u128 , core:: num:: NonZeroU128 , nonzero_check_new_unchecked_for_u128) ;
2436
2429
nonzero_check ! ( usize , core:: num:: NonZeroUsize , nonzero_check_new_unchecked_for_usize) ;
2437
2430
2438
- // macro_rules! nonzero_check_from_mut_unchecked {
2439
- // ($t:ty, $nonzero_type:ty, $harness_name:ident) => {
2440
- // #[kani::proof_for_contract(<T>::from_mut_unchecked)]
2441
- // pub fn $harness_name() {
2442
- // let mut x: $t = kani::any();
2443
- // unsafe {
2444
- // <$nonzero_type>::from_mut_unchecked(&mut x);
2445
- // }
2446
- // }
2447
- // };
2448
- // }
2449
-
2450
- // // Generate harnesses for multiple types
2451
- // nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8);
2452
- // nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16);
2453
- // nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32);
2454
- // nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64);
2455
- // nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128);
2456
- // nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize);
2457
- // nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8);
2458
- // nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16);
2459
- // nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32);
2460
- // nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64);
2461
- // nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128);
2462
- // nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize);
2463
-
2464
2431
macro_rules! nonzero_check_cmp {
2465
2432
( $nonzero_type: ty, $nonzero_check_cmp_for: ident) => {
2466
2433
#[ kani:: proof]
0 commit comments