@@ -8,15 +8,13 @@ use crate::hint::assert_unchecked;
8
8
use crate :: iter:: {
9
9
FusedIterator , TrustedLen , TrustedRandomAccess , TrustedRandomAccessNoCoerce , UncheckedIterator ,
10
10
} ;
11
+ #[ cfg( kani) ]
12
+ use crate :: kani;
11
13
use crate :: marker:: PhantomData ;
12
14
use crate :: mem:: { self , SizedTypeProperties } ;
13
15
use crate :: num:: NonZero ;
14
16
use crate :: ptr:: { self , without_provenance, without_provenance_mut, NonNull } ;
15
17
use crate :: { cmp, fmt} ;
16
-
17
- #[ cfg( kani) ]
18
- use crate :: kani;
19
-
20
18
use crate :: ub_checks:: Invariant ;
21
19
22
20
#[ stable( feature = "boxed_slice_into_iter" , since = "1.80.0" ) ]
@@ -163,14 +161,15 @@ impl<T> AsRef<[T]> for Iter<'_, T> {
163
161
}
164
162
165
163
#[ unstable( feature = "ub_checks" , issue = "none" ) ]
166
- impl < T > crate :: ub_checks :: Invariant for Iter < ' _ , T > {
164
+ impl < T > Invariant for Iter < ' _ , T > {
167
165
fn is_safe ( & self ) -> bool {
168
166
let ty_size = crate :: mem:: size_of :: < T > ( ) ;
169
167
let distance = self . ptr . addr ( ) . get ( ) . abs_diff ( self . end_or_len as usize ) ;
170
168
if ty_size == 0 || distance == 0 {
171
169
self . ptr . is_aligned ( )
172
170
} else {
173
- let slice_ptr: * const [ T ] = crate :: ptr:: from_raw_parts ( self . ptr . as_ptr ( ) , distance / ty_size) ;
171
+ let slice_ptr: * const [ T ] =
172
+ crate :: ptr:: from_raw_parts ( self . ptr . as_ptr ( ) , distance / ty_size) ;
174
173
crate :: ub_checks:: same_allocation ( self . ptr . as_ptr ( ) , self . end_or_len )
175
174
&& self . ptr . addr ( ) . get ( ) <= self . end_or_len as usize
176
175
&& distance % ty_size == 0
@@ -219,14 +218,15 @@ pub struct IterMut<'a, T: 'a> {
219
218
}
220
219
221
220
#[ unstable( feature = "ub_checks" , issue = "none" ) ]
222
- impl < T > crate :: ub_checks :: Invariant for IterMut < ' _ , T > {
221
+ impl < T > Invariant for IterMut < ' _ , T > {
223
222
fn is_safe ( & self ) -> bool {
224
223
let size = crate :: mem:: size_of :: < T > ( ) ;
225
224
if size == 0 {
226
225
self . ptr . is_aligned ( )
227
226
} else {
228
227
let distance = self . ptr . addr ( ) . get ( ) . abs_diff ( self . end_or_len as usize ) ;
229
- let slice_ptr: * mut [ T ] = crate :: ptr:: from_raw_parts_mut ( self . ptr . as_ptr ( ) , distance / size) ;
228
+ let slice_ptr: * mut [ T ] =
229
+ crate :: ptr:: from_raw_parts_mut ( self . ptr . as_ptr ( ) , distance / size) ;
230
230
crate :: ub_checks:: same_allocation ( self . ptr . as_ptr ( ) , self . end_or_len )
231
231
&& self . ptr . addr ( ) . get ( ) <= self . end_or_len as usize
232
232
&& distance % size == 0
@@ -3506,7 +3506,8 @@ impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> {
3506
3506
}
3507
3507
3508
3508
/// Verify the safety of the code implemented in this module (including generated code from macros).
3509
- #[ unstable( feature = "kani" , issue="none" ) ]
3509
+ #[ cfg( kani) ]
3510
+ #[ unstable( feature = "kani" , issue = "none" ) ]
3510
3511
mod verify {
3511
3512
use super :: * ;
3512
3513
use crate :: kani;
@@ -3604,17 +3605,29 @@ mod verify {
3604
3605
3605
3606
// check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any());
3606
3607
3607
- check_safe_abstraction!( check_is_empty, $ty, |iter: & mut Iter <' _, $ty>| { let _ = iter. is_empty( ) ; } ) ;
3608
- check_safe_abstraction!( check_len, $ty, |iter: & mut Iter <' _, $ty>| { let _ = iter. len( ) ; } ) ;
3609
- check_safe_abstraction!( check_size_hint, $ty, |iter: & mut Iter <' _, $ty>| { let _ = iter. size_hint( ) ; } ) ;
3608
+ check_safe_abstraction!( check_is_empty, $ty, |iter: & mut Iter <' _, $ty>| {
3609
+ let _ = iter. is_empty( ) ;
3610
+ } ) ;
3611
+ check_safe_abstraction!( check_len, $ty, |iter: & mut Iter <' _, $ty>| {
3612
+ let _ = iter. len( ) ;
3613
+ } ) ;
3614
+ check_safe_abstraction!( check_size_hint, $ty, |iter: & mut Iter <' _, $ty>| {
3615
+ let _ = iter. size_hint( ) ;
3616
+ } ) ;
3610
3617
//check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
3611
3618
//check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
3612
- //check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next_back(); });
3619
+ check_safe_abstraction!( check_next_back, $ty, |iter: & mut Iter <' _, $ty>| {
3620
+ let _ = iter. next_back( ) ;
3621
+ } ) ;
3613
3622
//check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
3614
- check_safe_abstraction!( check_next, $ty, |iter: & mut Iter <' _, $ty>| { let _ = iter. next( ) ; } ) ;
3623
+ check_safe_abstraction!( check_next, $ty, |iter: & mut Iter <' _, $ty>| {
3624
+ let _ = iter. next( ) ;
3625
+ } ) ;
3615
3626
3616
3627
// Ensure that clone always generates a safe object.
3617
- check_safe_abstraction!( check_clone, $ty, |iter: & mut Iter <' _, $ty>| { kani:: assert( iter. clone( ) . is_safe( ) , "Clone is safe" ) ; } ) ;
3628
+ check_safe_abstraction!( check_clone, $ty, |iter: & mut Iter <' _, $ty>| {
3629
+ kani:: assert( iter. clone( ) . is_safe( ) , "Clone is safe" ) ;
3630
+ } ) ;
3618
3631
}
3619
3632
} ;
3620
3633
}
@@ -3623,4 +3636,4 @@ mod verify {
3623
3636
check_iter_with_ty ! ( verify_u8, u8 , u32 :: MAX as usize ) ;
3624
3637
check_iter_with_ty ! ( verify_char, char , 50 ) ;
3625
3638
check_iter_with_ty ! ( verify_tup, ( char , u8 ) , 50 ) ;
3626
- }
3639
+ }
0 commit comments