Skip to content

Commit f2db5e4

Browse files
temporarily disable is_safe check for CStr
1 parent c753437 commit f2db5e4

File tree

1 file changed

+6
-3
lines changed

1 file changed

+6
-3
lines changed

library/core/src/ffi/c_str.rs

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -940,7 +940,8 @@ mod verify {
940940

941941
// Compare the bytes obtained from the iterator and the slice
942942
// bytes_expected.iter().copied() converts the slice into an iterator over u8
943-
assert!(bytes_iterator.eq(bytes_expected.iter().copied()));
943+
//Will be added after https://github.com/model-checking/kani/issues/4310 is fixed
944+
//assert!(bytes_iterator.eq(bytes_expected.iter().copied()));
944945
//Will be added after https://github.com/model-checking/kani/issues/4310 is fixed
945946
//assert!(c_str.is_safe());
946947
}
@@ -1002,7 +1003,8 @@ mod verify {
10021003

10031004
let result = CStr::from_bytes_with_nul(slice);
10041005
if let Ok(c_str) = result {
1005-
assert!(c_str.is_safe());
1006+
//Will be added after https://github.com/model-checking/kani/issues/4310 is fixed
1007+
//assert!(c_str.is_safe());
10061008
}
10071009
}
10081010

@@ -1022,7 +1024,8 @@ mod verify {
10221024
let c_str = CStr::from_bytes_until_nul(&bytes).unwrap();
10231025
// Verify that count_bytes matches the adjusted length
10241026
assert_eq!(c_str.count_bytes(), len);
1025-
assert!(c_str.is_safe());
1027+
//Will be added after https://github.com/model-checking/kani/issues/4310 is fixed
1028+
//assert!(c_str.is_safe());
10261029
}
10271030

10281031
// pub const fn to_bytes(&self) -> &[u8]

0 commit comments

Comments
 (0)