Harnesses for to_bytes and to_bytes_with_nul (#189)

Towards #150 

### Changes
* Added harnesses for `to_bytes` and `to_bytes_with_nul`
* Added a small fix to `count_bytes`

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

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

VERIFICATION:- SUCCESSFUL
Verification Time: 88.397385s

Checking harness ffi::c_str::verify::check_to_bytes...

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

VERIFICATION:- SUCCESSFUL
Verification Time: 79.66312s

Checking harness ffi::c_str::verify::check_from_bytes_until_nul...

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

VERIFICATION:- SUCCESSFUL
Verification Time: 28.593569s

Complete - 3 successfully verified harnesses, 0 failures, 3 total.
```

Author: Yenyun035

library/core/src/ffi/c_str.rs

@@ -859,6 +859,15 @@ impl FusedIterator for Bytes<'_> {}
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
+    
+    // Helper function
+    fn arbitrary_cstr(slice: &[u8]) -> &CStr {
+        let result = CStr::from_bytes_until_nul(&slice);
+        kani::assume(result.is_ok());
+        let c_str = result.unwrap();
+        assert!(c_str.is_safe());
+        c_str
+    }
 
     // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
     #[kani::proof]
@@ -875,7 +884,8 @@ mod verify {
             assert!(c_str.is_safe());
         }
     }
-
+  
+    // pub const fn count_bytes(&self) -> usize
     #[kani::proof]
     #[kani::unwind(32)]
     fn check_count_bytes() {
@@ -897,5 +907,38 @@ mod verify {
         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);
+        assert!(c_str.is_safe());
+    }
+
+    // pub const fn to_bytes(&self) -> &[u8]
+    #[kani::proof]
+    #[kani::unwind(32)]
+    fn check_to_bytes() {
+        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();
+        let end_idx = bytes.len();
+        // Comparison does not include the null byte
+        assert_eq!(bytes, &slice[..end_idx]);
+        assert!(c_str.is_safe());
+    }
+
+    // pub const fn to_bytes_with_nul(&self) -> &[u8]
+    #[kani::proof]
+    #[kani::unwind(33)]
+    fn check_to_bytes_with_nul() {
+        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_with_nul();
+        let end_idx = bytes.len();
+        // Comparison includes the null byte
+        assert_eq!(bytes, &slice[..end_idx]);
+        assert!(c_str.is_safe());
     }
 }