64
64
) ]
65
65
#![ allow( missing_docs) ]
66
66
67
- use crate :: marker:: { DiscriminantKind , Tuple } ;
68
- use crate :: mem:: SizedTypeProperties ;
69
- use crate :: { ptr, ub_checks} ;
70
67
use safety:: { ensures, requires} ;
71
68
72
69
#[ cfg( kani) ]
73
70
use crate :: kani;
71
+ use crate :: marker:: { DiscriminantKind , Tuple } ;
72
+ use crate :: mem:: SizedTypeProperties ;
73
+ use crate :: { ptr, ub_checks} ;
74
74
75
75
pub mod fallback;
76
76
pub mod mir;
@@ -4944,6 +4944,7 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
4944
4944
#[ unstable( feature = "kani" , issue = "none" ) ]
4945
4945
mod verify {
4946
4946
use core:: mem:: MaybeUninit ;
4947
+
4947
4948
use kani:: { AllocationStatus , Arbitrary , ArbitraryPointer , PointerGenerator } ;
4948
4949
4949
4950
use super :: * ;
@@ -4978,7 +4979,7 @@ mod verify {
4978
4979
// `copy_nonoverlapping`.
4979
4980
// Kani contract checking would fail due to existing restriction on calls to
4980
4981
// the function under verification.
4981
- let gen_any_ptr = |buf : & mut [ MaybeUninit < char > ; 100 ] | -> * mut char {
4982
+ let gen_any_ptr = |buf : & mut [ MaybeUninit < char > ; 100 ] | -> * mut char {
4982
4983
let base = buf. as_mut_ptr ( ) as * mut u8 ;
4983
4984
base. wrapping_add ( kani:: any_where ( |offset : & usize | * offset < 400 ) ) as * mut char
4984
4985
} ;
@@ -4993,13 +4994,13 @@ mod verify {
4993
4994
let dst = if kani:: any ( ) { gen_any_ptr ( & mut buffer2) } else { gen_any_ptr ( & mut buffer1) } ;
4994
4995
unsafe { copy_nonoverlapping ( src, dst, kani:: any ( ) ) }
4995
4996
}
4996
-
4997
- //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does
4997
+
4998
+ //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does
4998
4999
//not currently support contracts (https://github.com/model-checking/kani/issues/3345)
4999
5000
#[ requires( crate :: mem:: size_of:: <T >( ) == crate :: mem:: size_of:: <U >( ) ) ] //T and U have same size (transmute_unchecked does not guarantee this)
5000
5001
#[ requires( ub_checks:: can_dereference( & input as * const T as * const U ) ) ] //output can be deref'd as value of type U
5001
5002
#[ allow( dead_code) ]
5002
- unsafe fn transmute_unchecked_wrapper < T , U > ( input : T ) -> U {
5003
+ unsafe fn transmute_unchecked_wrapper < T , U > ( input : T ) -> U {
5003
5004
unsafe { transmute_unchecked ( input) }
5004
5005
}
5005
5006
@@ -5055,7 +5056,7 @@ mod verify {
5055
5056
//tests that transmute works correctly when transmuting something with zero size
5056
5057
#[ kani:: proof_for_contract( transmute_unchecked_wrapper) ]
5057
5058
fn transmute_zero_size ( ) {
5058
- let empty_arr: [ u8 ; 0 ] = [ ] ;
5059
+ let empty_arr: [ u8 ; 0 ] = [ ] ;
5059
5060
let unit_val: ( ) = unsafe { transmute_unchecked_wrapper ( empty_arr) } ;
5060
5061
assert ! ( unit_val == ( ) ) ;
5061
5062
}
@@ -5073,7 +5074,7 @@ mod verify {
5073
5074
let src: $src = kani:: any( ) ;
5074
5075
let dst: $dst = unsafe { transmute_unchecked_wrapper( src) } ;
5075
5076
let src2: $src = unsafe { transmute_unchecked_wrapper( dst) } ;
5076
- assert_eq!( src, src2) ;
5077
+ assert_eq!( src, src2) ;
5077
5078
}
5078
5079
} ;
5079
5080
}
@@ -5101,28 +5102,17 @@ mod verify {
5101
5102
#[ kani:: proof_for_contract( write_bytes) ]
5102
5103
fn check_write_bytes ( ) {
5103
5104
let mut generator = PointerGenerator :: < 100 > :: new ( ) ;
5104
- let ArbitraryPointer {
5105
- ptr,
5106
- status,
5107
- ..
5108
- } = generator. any_alloc_status :: < char > ( ) ;
5105
+ let ArbitraryPointer { ptr, status, .. } = generator. any_alloc_status :: < char > ( ) ;
5109
5106
kani:: assume ( supported_status ( status) ) ;
5110
5107
unsafe { write_bytes ( ptr, kani:: any ( ) , kani:: any ( ) ) } ;
5111
5108
}
5112
5109
5113
5110
fn run_with_arbitrary_ptrs < T : Arbitrary > ( harness : impl Fn ( * mut T , * mut T ) ) {
5114
5111
let mut generator1 = PointerGenerator :: < 100 > :: new ( ) ;
5115
5112
let mut generator2 = PointerGenerator :: < 100 > :: new ( ) ;
5116
- let ArbitraryPointer {
5117
- ptr : src,
5118
- status : src_status,
5119
- ..
5120
- } = generator1. any_alloc_status :: < T > ( ) ;
5121
- let ArbitraryPointer {
5122
- ptr : dst,
5123
- status : dst_status,
5124
- ..
5125
- } = if kani:: any ( ) {
5113
+ let ArbitraryPointer { ptr : src, status : src_status, .. } =
5114
+ generator1. any_alloc_status :: < T > ( ) ;
5115
+ let ArbitraryPointer { ptr : dst, status : dst_status, .. } = if kani:: any ( ) {
5126
5116
generator1. any_alloc_status :: < T > ( )
5127
5117
} else {
5128
5118
generator2. any_alloc_status :: < T > ( )
0 commit comments