Skip to content

Commit 8f83c58

Browse files
authored
Merge branch 'main' into c-0013-rajathm-bytes-as_ptr-to_str
2 parents 7372ed6 + d0d9de2 commit 8f83c58

File tree

3 files changed

+455
-13
lines changed

3 files changed

+455
-13
lines changed

library/core/src/ffi/c_str.rs

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -948,6 +948,19 @@ mod verify {
948948
assert!(c_str.is_safe());
949949
}
950950

951+
#[kani::proof]
952+
#[kani::unwind(17)]
953+
fn check_from_bytes_with_nul() {
954+
const MAX_SIZE: usize = 16;
955+
let string: [u8; MAX_SIZE] = kani::any();
956+
let slice = kani::slice::any_slice_of_array(&string);
957+
958+
let result = CStr::from_bytes_with_nul(slice);
959+
if let Ok(c_str) = result {
960+
assert!(c_str.is_safe());
961+
}
962+
}
963+
951964
// pub const fn count_bytes(&self) -> usize
952965
#[kani::proof]
953966
#[kani::unwind(32)]

0 commit comments

Comments
 (0)