Address comments

qinheping · Nov 8, 2024 · aa177cc · aa177cc
1 parent 4d1a924
commit aa177cc
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs
@@ -230,6 +230,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
+// Required for Kani loop contracts, which are annotated as custom stmt attributes.
 #![feature(proc_macro_hygiene)]
 // tidy-alphabetical-end
 //

diff --git a/library/core/src/str/validations.rs b/library/core/src/str/validations.rs
@@ -284,10 +284,9 @@ pub mod verify {
     use super::*;
 
     #[kani::proof]
-    #[kani::unwind(8)]
     pub fn check_run_utf8_validation() {
         if kani::any() {
-            // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument
+            // TODO: ARR_SIZE can be much larger with cbmc argument
             // `--arrays-uf-always`
             const ARR_SIZE: usize = 1000;
             let mut x: [u8; ARR_SIZE] = kani::any();