back to unwind

Author: thanhnguyen-aws

library/core/src/ffi/c_str.rs

@@ -891,7 +891,7 @@ mod verify {
 
     // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_from_bytes_until_nul() {
         const MAX_SIZE: usize = 32;
@@ -908,7 +908,7 @@ mod verify {
 
     //  pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr
     #[kani::proof_for_contract(CStr::from_bytes_with_nul_unchecked)]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     fn check_from_bytes_with_nul_unchecked() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -927,7 +927,7 @@ mod verify {
 
     // pub fn bytes(&self) -> Bytes<'_>
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_bytes() {
         const MAX_SIZE: usize = 32;
@@ -946,7 +946,7 @@ mod verify {
 
     // pub const fn to_str(&self) -> Result<&str, str::Utf8Error>
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_to_str() {
         const MAX_SIZE: usize = 32;
@@ -964,7 +964,7 @@ mod verify {
 
     // pub const fn as_ptr(&self) -> *const c_char
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_as_ptr() {
         const MAX_SIZE: usize = 32;
@@ -992,7 +992,7 @@ mod verify {
 
     // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError>
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_from_bytes_with_nul() {
         const MAX_SIZE: usize = 16;
@@ -1007,7 +1007,7 @@ mod verify {
 
     // pub const fn count_bytes(&self) -> usize
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_count_bytes() {
         const MAX_SIZE: usize = 32;
@@ -1033,7 +1033,7 @@ mod verify {
 
     // pub const fn to_bytes(&self) -> &[u8]
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_to_bytes() {
         const MAX_SIZE: usize = 32;
@@ -1050,7 +1050,7 @@ mod verify {
 
     // pub const fn to_bytes_with_nul(&self) -> &[u8]
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_to_bytes_with_nul() {
         const MAX_SIZE: usize = 32;
@@ -1067,7 +1067,7 @@ mod verify {
 
     // const unsafe fn strlen(ptr: *const c_char) -> usize
     #[kani::proof_for_contract(super::strlen)]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_strlen_contract() {
         const MAX_SIZE: usize = 32;
@@ -1081,7 +1081,7 @@ mod verify {
 
     // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr
     #[kani::proof_for_contract(CStr::from_ptr)]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_from_ptr_contract() {
         const MAX_SIZE: usize = 32;
@@ -1095,7 +1095,7 @@ mod verify {
 
     // pub const fn is_empty(&self) -> bool
     #[kani::proof]
-    #[kani::solver(cvc5)]
+    #[kani::unwind(32)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     fn check_is_empty() {
         const MAX_SIZE: usize = 32;