From 7e8a03d361af17f1db3d3fe7be9501589fd5a01a Mon Sep 17 00:00:00 2001
From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com>
Date: Sun, 1 Dec 2024 12:59:07 -0800
Subject: [PATCH] Harness for `CStr::is_empty` (#194)

Towards #150

### Changes
* Added a harness for `is_empty`
* Added a small optimization for `arbitray_cstr`

### Verification Result
```
SUMMARY:
 ** 0 of 193 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 51.462265s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
```
---
 library/core/src/ffi/c_str.rs | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
index 328c7276a22e8..fe97ed3e5f2fb 100644
--- a/library/core/src/ffi/c_str.rs
+++ b/library/core/src/ffi/c_str.rs
@@ -860,8 +860,11 @@ mod verify {
     
     // Helper function
     fn arbitrary_cstr(slice: &[u8]) -> &CStr {
+        // At a minimum, the slice has a null terminator to form a valid CStr.
+        kani::assume(slice.len() > 0 && slice[slice.len() - 1] == 0);
         let result = CStr::from_bytes_until_nul(&slice);
-        kani::assume(result.is_ok());
+        // Given the assumption, from_bytes_until_nul should never fail
+        assert!(result.is_ok());
         let c_str = result.unwrap();
         assert!(c_str.is_safe());
         c_str
@@ -939,4 +942,18 @@ mod verify {
         assert_eq!(bytes, &slice[..end_idx]);
         assert!(c_str.is_safe());
     }
+  
+    #[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);
+        let c_str = arbitrary_cstr(slice);
+
+        let bytes = c_str.to_bytes(); // does not include null terminator
+        let expected_is_empty = bytes.len() == 0;
+        assert_eq!(expected_is_empty, c_str.is_empty());
+        assert!(c_str.is_safe());
+  }
 }
\ No newline at end of file