From f87b1aec2b0489b90c719ddb8b63caa19d2305d1 Mon Sep 17 00:00:00 2001
From: MWDZ <101102544+MWDZ@users.noreply.github.com>
Date: Thu, 28 Nov 2024 03:00:49 -0800
Subject: [PATCH] Harnesses for `count_bytes`  (#191)

Towards #150

Changes
Added harnesses for count_bytes

Verification Result
```
Checking harness ffi::c_str::verify::check_count_bytes...

VERIFICATION RESULT:
 ** 0 of 241 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 5.377671s
```
---
 library/core/src/ffi/c_str.rs | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
index 2a65b2415f7d3..05506aa4fb19d 100644
--- a/library/core/src/ffi/c_str.rs
+++ b/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);
+    }
 }
\ No newline at end of file