Harnesses for to_bytes and to_bytes_with_nul

library/core/src/ffi/c_str.rs

@@ -875,4 +875,42 @@ mod verify {
             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 result = CStr::from_bytes_until_nul(slice);
+        if let Ok(c_str) = result {
+            // Find the index of the first null byte in the slice since
+            // from_bytes_until_nul stops by there
+            let end_idx = slice.iter().position(|x| *x == 0).unwrap();
+            // Comparison does not include the null byte
+            assert_eq!(c_str.to_bytes(), &slice[..end_idx]);
+            assert!(c_str.is_safe());
+        }
+    }
+
+    // pub const fn to_bytes_with_nul(&self) -> &[u8]
+    #[kani::proof]
+    #[kani::unwind(33)] // 101.7 seconds when 33; 17.9 seconds for 17
+    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 result = CStr::from_bytes_until_nul(slice);
+        if let Ok(c_str) = result {
+            // Find the index of the first null byte in the slice since
+            // from_bytes_until_nul stops by there
+            let end_idx = slice.iter().position(|x| *x == 0).unwrap();
+            // Comparison includes the null byte
+            assert_eq!(c_str.to_bytes_with_nul(), &slice[..end_idx + 1]);
+            assert!(c_str.is_safe());
+        }
+    }
 }