added harnesses for c_str: is_empty

library/core/src/ffi/c_str.rs

@@ -875,4 +875,50 @@ mod verify {
             assert!(c_str.is_safe());
         }
     }
+
+    #[kani::proof]
+    #[kani::unwind(32)]
+    fn check_count_bytes() {
+        const MAX_SIZE: usize = 32;
+        let mut bytes: [u8; MAX_SIZE] = kani::any();
+
+        // Non-deterministically generate a length within the valid range [0, MAX_SIZE]
+        let mut len: usize = kani::any_where(|&x| x < MAX_SIZE);
+
+        // If a null byte exists before the generated length
+        // adjust len to its position
+        if let Some(pos) = bytes[..len].iter().position(|&x| x == 0) {
+            len = pos;
+        } else {
+            // If no null byte, insert one at the chosen length
+            bytes[len] = 0;
+        }
+
+        let c_str = CStr::from_bytes_until_nul(&bytes).unwrap();
+        // Verify that count_bytes matches the adjusted length
+        assert_eq!(c_str.count_bytes(), len);
+    }
+
+    /// Verifies the `CStr::is_empty` method.
+    #[kani::proof]
+    #[kani::unwind(33)]
+    fn check_is_empty() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        // Attempt to create a CStr and handle possible failure
+        if let Ok(c_str) = CStr::from_bytes_with_nul(slice) {
+            // Validate the safety of the constructed CStr
+            assert!(c_str.is_safe(), "Constructed CStr failed the safety invariant.");
+
+            // Test the is_empty method
+            let bytes = c_str.to_bytes(); // Excludes the null terminator
+            let expected_is_empty = bytes.len() == 0;
+            assert_eq!(expected_is_empty, c_str.is_empty());
+        } else {
+            // If the slice is invalid, confirm that constructing CStr fails
+            assert!(slice.last() != Some(&0) || slice[..slice.len() - 1].contains(&0));
+        }
+    }
 }