@@ -893,18 +893,15 @@ mod verify {
893
893
const MAX_SIZE : usize = 32 ;
894
894
let string: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
895
895
let slice = kani:: slice:: any_slice_of_array ( & string) ;
896
+ let c_str = arbitrary_cstr ( slice) ;
896
897
897
- let result = CStr :: from_bytes_until_nul ( slice) ;
898
- if let Ok ( c_str) = result {
899
- let bytes_iterator = c_str. bytes ( ) ;
900
- let bytes_expected = c_str. to_bytes ( ) ;
901
-
902
- // Compare the bytes obtained from the iterator and the slice
903
- // bytes_expected.iter().copied() converts the slice into an iterator over u8
904
- assert ! ( bytes_iterator. eq( bytes_expected. iter( ) . copied( ) ) ) ;
898
+ let bytes_iterator = c_str. bytes ( ) ;
899
+ let bytes_expected = c_str. to_bytes ( ) ;
905
900
906
- assert ! ( c_str. is_safe( ) ) ;
907
- }
901
+ // Compare the bytes obtained from the iterator and the slice
902
+ // bytes_expected.iter().copied() converts the slice into an iterator over u8
903
+ assert ! ( bytes_iterator. eq( bytes_expected. iter( ) . copied( ) ) ) ;
904
+ assert ! ( c_str. is_safe( ) ) ;
908
905
}
909
906
910
907
// pub const fn to_str(&self) -> Result<&str, str::Utf8Error>
@@ -914,16 +911,14 @@ mod verify {
914
911
const MAX_SIZE : usize = 32 ;
915
912
let string: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
916
913
let slice = kani:: slice:: any_slice_of_array ( & string) ;
914
+ let c_str = arbitrary_cstr ( slice) ;
917
915
918
- let result = CStr :: from_bytes_until_nul ( slice) ;
919
- if let Ok ( c_str) = result {
920
- // a double conversion here and assertion, if the bytes are still the same, function is valid
921
- let str_result = c_str. to_str ( ) ;
922
- if let Ok ( s) = str_result {
923
- assert_eq ! ( s. as_bytes( ) , c_str. to_bytes( ) ) ;
924
- }
925
- assert ! ( c_str. is_safe( ) ) ;
916
+ // a double conversion here and assertion, if the bytes are still the same, function is valid
917
+ let str_result = c_str. to_str ( ) ;
918
+ if let Ok ( s) = str_result {
919
+ assert_eq ! ( s. as_bytes( ) , c_str. to_bytes( ) ) ;
926
920
}
921
+ assert ! ( c_str. is_safe( ) ) ;
927
922
}
928
923
929
924
// pub const fn as_ptr(&self) -> *const c_char
@@ -933,26 +928,24 @@ mod verify {
933
928
const MAX_SIZE : usize = 32 ;
934
929
let string: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
935
930
let slice = kani:: slice:: any_slice_of_array ( & string) ;
931
+ let c_str = arbitrary_cstr ( slice) ;
936
932
937
- let result = CStr :: from_bytes_until_nul ( slice) ;
938
- if let Ok ( c_str) = result {
939
- let ptr = c_str. as_ptr ( ) ;
940
- let bytes_with_nul = c_str. to_bytes_with_nul ( ) ;
941
- let len = bytes_with_nul. len ( ) ;
942
-
943
- // We ensure that `ptr` is valid for reads of `len` bytes
944
- unsafe {
945
- for i in 0 ..len {
946
- // Iterate and get each byte in the C string from our raw ptr
947
- let byte_at_ptr = * ptr. add ( i) ;
948
- // Get the byte at every pos
949
- let byte_in_cstr = bytes_with_nul[ i] ;
950
- // Compare the two bytes to ensure they are equal
951
- assert_eq ! ( byte_at_ptr as u8 , byte_in_cstr) ;
952
- }
933
+ let ptr = c_str. as_ptr ( ) ;
934
+ let bytes_with_nul = c_str. to_bytes_with_nul ( ) ;
935
+ let len = bytes_with_nul. len ( ) ;
936
+
937
+ // We ensure that `ptr` is valid for reads of `len` bytes
938
+ unsafe {
939
+ for i in 0 ..len {
940
+ // Iterate and get each byte in the C string from our raw ptr
941
+ let byte_at_ptr = * ptr. add ( i) ;
942
+ // Get the byte at every pos
943
+ let byte_in_cstr = bytes_with_nul[ i] ;
944
+ // Compare the two bytes to ensure they are equal
945
+ assert_eq ! ( byte_at_ptr as u8 , byte_in_cstr) ;
953
946
}
954
- assert ! ( c_str. is_safe( ) ) ;
955
947
}
948
+ assert ! ( c_str. is_safe( ) ) ;
956
949
}
957
950
958
951
// pub const fn count_bytes(&self) -> usize
0 commit comments