@@ -2070,7 +2070,7 @@ mod verify {
2070
2070
check_const_offset_from_tuple_4_arr
2071
2071
) ;
2072
2072
2073
- // Proof for contact of byte_offset_from to verify unit type
2073
+ // Proof for contact of byte_offset_from to verify unit type
2074
2074
#[ kani:: proof_for_contract( <* const ( ) >:: byte_offset_from) ]
2075
2075
pub fn check_const_byte_offset_from_unit ( ) {
2076
2076
let val: ( ) = ( ) ;
@@ -2081,7 +2081,7 @@ mod verify {
2081
2081
}
2082
2082
}
2083
2083
2084
- // generate proofs for contracts for byte_offset_from to verify int and composite
2084
+ // generate proofs for contracts for byte_offset_from to verify int and composite
2085
2085
// types
2086
2086
// - `$type`: pointee type
2087
2087
// - `$proof_name1`: name of the harness for single element
@@ -2222,7 +2222,8 @@ mod verify {
2222
2222
const gen_size: usize = mem:: size_of:: <$type>( ) ;
2223
2223
let mut generator1 = PointerGenerator :: <{ gen_size * ARRAY_LEN } >:: new( ) ;
2224
2224
let mut generator2 = PointerGenerator :: <{ gen_size * ARRAY_LEN } >:: new( ) ;
2225
- let ptr1: * const [ $type] = generator1. any_in_bounds( ) . ptr as * const [ $type; SLICE_LEN ] ;
2225
+ let ptr1: * const [ $type] =
2226
+ generator1. any_in_bounds( ) . ptr as * const [ $type; SLICE_LEN ] ;
2226
2227
let ptr2: * const [ $type] = if kani:: any( ) {
2227
2228
generator1. any_alloc_status( ) . ptr as * const [ $type; SLICE_LEN ]
2228
2229
} else {
@@ -2235,7 +2236,7 @@ mod verify {
2235
2236
}
2236
2237
} ;
2237
2238
}
2238
-
2239
+
2239
2240
generate_const_byte_offset_from_slice_harness ! ( u8 , check_const_byte_offset_from_u8_slice) ;
2240
2241
generate_const_byte_offset_from_slice_harness ! ( u16 , check_const_byte_offset_from_u16_slice) ;
2241
2242
generate_const_byte_offset_from_slice_harness ! ( u32 , check_const_byte_offset_from_u32_slice) ;
@@ -2248,5 +2249,4 @@ mod verify {
2248
2249
generate_const_byte_offset_from_slice_harness ! ( i64 , check_const_byte_offset_from_i64_slice) ;
2249
2250
generate_const_byte_offset_from_slice_harness ! ( i128 , check_const_byte_offset_from_i128_slice) ;
2250
2251
generate_const_byte_offset_from_slice_harness ! ( isize , check_const_byte_offset_from_isize_slice) ;
2251
-
2252
2252
}
0 commit comments