Cstr - add proof from_bytes_with_null

library/core/src/ffi/c_str.rs

@@ -882,6 +882,34 @@ mod verify {
             assert!(c_str.is_safe());
         }
     }
+
+    #[kani::proof]
+    #[kani::unwind(33)] 
+    fn check_from_bytes_with_nul() {
+        const MAX_SIZE: usize = 32;
+        let mut buffer: [u8; MAX_SIZE] = kani::any();
+
+        // Iterate over all possible slice lengths from 1 to MAX_SIZE
+        for slice_length in 1..=MAX_SIZE {
+            // Ensure the slice is valid by setting the last byte to null
+            buffer[slice_length - 1] = 0;
+
+            // Assume all bytes before the last are non-null
+            for i in 0..slice_length - 1 {
+                kani::assume(buffer[i] != 0);
+            }
+
+            // Create the slice up to the current slice_length
+            let slice = &buffer[..slice_length];
+            let result = CStr::from_bytes_with_nul(slice);
+
+            if let Ok(c_str) = result {
+                assert!(c_str.is_safe());
+                assert_eq!(c_str.to_bytes(), &buffer[..slice_length - 1]);
+                assert_eq!(c_str.to_bytes_with_nul(), &buffer[..slice_length]);
+            } 
+        }
+    }
 
     // pub const fn count_bytes(&self) -> usize
     #[kani::proof]
@@ -939,4 +967,4 @@ mod verify {
         assert_eq!(bytes, &slice[..end_idx]);
         assert!(c_str.is_safe());
     }
-}
+}