Merge branch 'model-checking:main' into transmute_unchecked

model-checking · Dec 3, 2024 · f813be8 · f813be8
2 parents a35f8a1 + d0d9de2
commit f813be8
Show file tree

Hide file tree

Showing 3 changed files with 503 additions and 16 deletions.
diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
@@ -885,7 +885,20 @@ mod verify {
             assert!(c_str.is_safe());
         }
     }
-
+
+    #[kani::proof]
+    #[kani::unwind(17)] 
+    fn check_from_bytes_with_nul() {
+        const MAX_SIZE: usize = 16;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        let result = CStr::from_bytes_with_nul(slice);
+        if let Ok(c_str) = result {
+            assert!(c_str.is_safe());
+        }
+    }
+
     // pub const fn count_bytes(&self) -> usize
     #[kani::proof]
     #[kani::unwind(32)]
@@ -956,4 +969,4 @@ mod verify {
         assert_eq!(expected_is_empty, c_str.is_empty());
         assert!(c_str.is_safe());
   }
-}
+}