Address comments

Author: qinheping

Diff for: 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 for: 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();