@@ -16,8 +16,12 @@ use core::cmp::Ordering::{self, Less};
16
16
use core:: kani;
17
17
#[ cfg( not( no_global_oom_handling) ) ]
18
18
use core:: mem:: MaybeUninit ;
19
+ #[ cfg( kani) ]
20
+ use core:: mem:: SizedTypeProperties ;
19
21
#[ cfg( not( no_global_oom_handling) ) ]
20
22
use core:: ptr;
23
+ #[ cfg( kani) ]
24
+ use core:: ptr:: slice_from_raw_parts;
21
25
#[ unstable( feature = "array_windows" , issue = "75027" ) ]
22
26
pub use core:: slice:: ArrayWindows ;
23
27
#[ stable( feature = "inherent_ascii_escape" , since = "1.60.0" ) ]
@@ -54,12 +58,6 @@ pub use core::slice::{from_mut_ptr_range, from_ptr_range};
54
58
pub use core:: slice:: { from_raw_parts, from_raw_parts_mut} ;
55
59
#[ unstable( feature = "slice_range" , issue = "76393" ) ]
56
60
pub use core:: slice:: { range, try_range} ;
57
- #[ cfg( kani) ]
58
- use crate :: kani;
59
- #[ cfg( kani) ]
60
- use core:: ptr:: slice_from_raw_parts;
61
- #[ cfg( kani) ]
62
- use core:: mem:: SizedTypeProperties ;
63
61
64
62
////////////////////////////////////////////////////////////////////////////////
65
63
// Basic slice extension methods
@@ -70,6 +68,8 @@ use crate::alloc::Global;
70
68
#[ cfg( not( no_global_oom_handling) ) ]
71
69
use crate :: borrow:: ToOwned ;
72
70
use crate :: boxed:: Box ;
71
+ #[ cfg( kani) ]
72
+ use crate :: kani;
73
73
use crate :: vec:: Vec ;
74
74
75
75
impl < T > [ T ] {
@@ -535,7 +535,7 @@ impl<T> [T] {
535
535
#[ cfg( kani) ]
536
536
let buf_ptr = ptr:: slice_from_raw_parts ( buf. as_ptr ( ) , capacity) ;
537
537
#[ cfg( kani) ]
538
- let len_ptr = unsafe { ( & buf as * const Vec < T > as * const usize ) . add ( 2 ) } ;
538
+ let len_ptr = unsafe { ( & buf as * const Vec < T > as * const usize ) . add ( 2 ) } ;
539
539
#[ safety:: loop_invariant(
540
540
kani:: mem:: same_allocation( buf. as_ptr( ) , buf. as_ptr( ) . wrapping_add( capacity) ) &&
541
541
unsafe { * len_ptr <= T :: MAX_SLICE_LEN } &&
0 commit comments