1
1
//! [`CStr`] and its related types.
2
2
3
+ use safety:: { ensures, requires} ;
4
+
3
5
use crate :: cmp:: Ordering ;
4
6
use crate :: error:: Error ;
5
7
use crate :: ffi:: c_char;
6
8
use crate :: intrinsics:: const_eval_select;
7
9
use crate :: iter:: FusedIterator ;
10
+ #[ cfg( kani) ]
11
+ use crate :: kani;
8
12
use crate :: marker:: PhantomData ;
9
13
use crate :: ptr:: NonNull ;
10
14
use crate :: slice:: memchr;
11
- use crate :: { fmt, ops, slice, str} ;
12
- use safety:: { requires, ensures} ;
13
-
14
15
use crate :: ub_checks:: Invariant ;
15
16
#[ allow( unused_imports) ]
16
17
use crate :: ub_checks:: can_dereference;
17
-
18
- #[ cfg( kani) ]
19
- use crate :: kani;
18
+ use crate :: { fmt, ops, slice, str} ;
20
19
21
20
// FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link
22
21
// depends on where the item is being documented. however, since this is libcore, we can't
@@ -228,7 +227,7 @@ impl Invariant for &CStr {
228
227
let bytes: & [ c_char ] = & self . inner ;
229
228
let len = bytes. len ( ) ;
230
229
231
- !bytes. is_empty ( ) && bytes[ len - 1 ] == 0 && !bytes[ ..len- 1 ] . contains ( & 0 )
230
+ !bytes. is_empty ( ) && bytes[ len - 1 ] == 0 && !bytes[ ..len - 1 ] . contains ( & 0 )
232
231
}
233
232
}
234
233
@@ -887,7 +886,7 @@ impl FusedIterator for Bytes<'_> {}
887
886
#[ unstable( feature = "kani" , issue = "none" ) ]
888
887
mod verify {
889
888
use super :: * ;
890
-
889
+
891
890
// Helper function
892
891
fn arbitrary_cstr ( slice : & [ u8 ] ) -> & CStr {
893
892
// At a minimum, the slice has a null terminator to form a valid CStr.
@@ -934,7 +933,7 @@ mod verify {
934
933
let len = bytes. len ( ) ;
935
934
assert_eq ! ( bytes, & slice[ ..len] ) ;
936
935
}
937
-
936
+
938
937
// pub fn bytes(&self) -> Bytes<'_>
939
938
#[ kani:: proof]
940
939
#[ kani:: unwind( 32 ) ]
@@ -972,7 +971,7 @@ mod verify {
972
971
973
972
// pub const fn as_ptr(&self) -> *const c_char
974
973
#[ kani:: proof]
975
- #[ kani:: unwind( 33 ) ]
974
+ #[ kani:: unwind( 33 ) ]
976
975
fn check_as_ptr ( ) {
977
976
const MAX_SIZE : usize = 32 ;
978
977
let string: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
@@ -996,10 +995,10 @@ mod verify {
996
995
}
997
996
assert ! ( c_str. is_safe( ) ) ;
998
997
}
999
-
998
+
1000
999
// pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError>
1001
1000
#[ kani:: proof]
1002
- #[ kani:: unwind( 17 ) ]
1001
+ #[ kani:: unwind( 17 ) ]
1003
1002
fn check_from_bytes_with_nul ( ) {
1004
1003
const MAX_SIZE : usize = 16 ;
1005
1004
let string: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
@@ -1017,10 +1016,10 @@ mod verify {
1017
1016
fn check_count_bytes ( ) {
1018
1017
const MAX_SIZE : usize = 32 ;
1019
1018
let mut bytes: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
1020
-
1019
+
1021
1020
// Non-deterministically generate a length within the valid range [0, MAX_SIZE]
1022
1021
let mut len: usize = kani:: any_where ( |& x| x < MAX_SIZE ) ;
1023
-
1022
+
1024
1023
// If a null byte exists before the generated length
1025
1024
// adjust len to its position
1026
1025
if let Some ( pos) = bytes[ ..len] . iter ( ) . position ( |& x| x == 0 ) {
@@ -1029,7 +1028,7 @@ mod verify {
1029
1028
// If no null byte, insert one at the chosen length
1030
1029
bytes[ len] = 0 ;
1031
1030
}
1032
-
1031
+
1033
1032
let c_str = CStr :: from_bytes_until_nul ( & bytes) . unwrap ( ) ;
1034
1033
// Verify that count_bytes matches the adjusted length
1035
1034
assert_eq ! ( c_str. count_bytes( ) , len) ;
@@ -1076,7 +1075,9 @@ mod verify {
1076
1075
let mut string: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
1077
1076
let ptr = string. as_ptr ( ) as * const c_char ;
1078
1077
1079
- unsafe { super :: strlen ( ptr) ; }
1078
+ unsafe {
1079
+ super :: strlen ( ptr) ;
1080
+ }
1080
1081
}
1081
1082
1082
1083
// pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr
@@ -1087,9 +1088,11 @@ mod verify {
1087
1088
let string: [ u8 ; MAX_SIZE ] = kani:: any ( ) ;
1088
1089
let ptr = string. as_ptr ( ) as * const c_char ;
1089
1090
1090
- unsafe { CStr :: from_ptr ( ptr) ; }
1091
+ unsafe {
1092
+ CStr :: from_ptr ( ptr) ;
1093
+ }
1091
1094
}
1092
-
1095
+
1093
1096
// pub const fn is_empty(&self) -> bool
1094
1097
#[ kani:: proof]
1095
1098
#[ kani:: unwind( 33 ) ]
0 commit comments