Harnesses for count_bytes

library/core/src/ffi/c_str.rs

@@ -875,4 +875,27 @@ 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);
+    }
 }