Update Kani version

Author: qinheping

library/core/src/alloc/layout.rs

@@ -655,7 +655,7 @@ mod verify {
     }
 
     // pub const fn size(&self) -> usize
-    //#[kani::proof]
+    #[kani::proof]
     pub fn check_size() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
@@ -667,7 +667,7 @@ mod verify {
     }
 
     // pub const fn align(&self) -> usize
-    //#[kani::proof]
+    #[kani::proof]
     pub fn check_align() {
         let layout = kani::any::<Layout>();
         assert!(layout.align().is_power_of_two());

library/core/src/lib.rs

@@ -230,7 +230,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
-#![cfg_attr(kani, feature(proc_macro_hygiene))]
+#![feature(proc_macro_hygiene)]
 // tidy-alphabetical-end
 //
 // Target features:

library/core/src/num/mod.rs

@@ -1770,7 +1770,7 @@ mod verify {
     macro_rules! generate_carrying_mul_intervals {
         ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
             $(
-                //#[kani::proof]
+                #[kani::proof]
                 pub fn $harness_name() {
                     let lhs: $type = kani::any::<$type>();
                     let rhs: $type = kani::any::<$type>();
@@ -1807,7 +1807,7 @@ mod verify {
     macro_rules! generate_widening_mul_intervals {
         ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
             $(
-                //#[kani::proof]
+                #[kani::proof]
                 pub fn $harness_name() {
                     let lhs: $type = kani::any::<$type>();
                     let rhs: $type = kani::any::<$type>();

library/core/src/ptr/unique.rs

@@ -263,7 +263,7 @@ mod verify {
     }
 
     // pub const unsafe fn as_ref(&self) -> &T
-    //#[kani::proof]
+    #[kani::proof]
     pub fn check_as_ref() {
         let mut x : i32 = kani::any();
         let xptr = &mut x;
@@ -274,7 +274,7 @@ mod verify {
     }
 
     // pub const unsafe fn as_mut(&mut self) -> &mut T
-    //#[kani::proof]
+    #[kani::proof]
     pub fn check_as_mut() {
         let mut x : i32 = kani::any();
         let xptr = &mut x;
@@ -285,7 +285,7 @@ mod verify {
     }
 
     // pub const fn cast<U>(self) -> Unique<U>
-    //#[kani::proof]
+    #[kani::proof]
     pub fn check_cast() {
         let mut x : i32 = kani::any();
         let xptr = &mut x;

library/core/src/str/pattern.rs

@@ -43,7 +43,8 @@ use crate::convert::TryInto as _;
 use crate::slice::memchr;
 use crate::{cmp, fmt};
 
-use safety::{requires, ensures};
+#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] // only called on x86
+use safety::{loop_invariant, requires};
 
 #[cfg(kani)]
 use crate::kani;
@@ -1959,7 +1960,7 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
     unsafe {
         let (mut px, mut py) = (x.as_ptr(), y.as_ptr());
         let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4));
-        #[safety::loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py)
+        #[loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py)
         && px as isize >= x.as_ptr() as isize
         && py as isize >= y.as_ptr() as isize
         && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))]
@@ -1987,7 +1988,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(4)]
     pub fn check_small_slice_eq() {
-        // ARR_SIZE can `std::usize::MAX` with cbmc argument
+        // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument
         // `--arrays-uf-always`
         const ARR_SIZE: usize = 1000;
         let x: [u8; ARR_SIZE] = kani::any();

library/core/src/unicode/mod.rs

@@ -38,13 +38,13 @@ mod verify {
     use crate::kani;
 
     /// Checks that `to_upper` does not trigger UB or panics for all valid characters.
-    //#[kani::proof]
+    #[kani::proof]
     fn check_to_upper_safety() {
         let _ = to_upper(kani::any());
     }
 
     /// Checks that `to_lower` does not trigger UB or panics for all valid characters.
-    //#[kani::proof]
+    #[kani::proof]
     fn check_to_lower_safety() {
         let _ = to_lower(kani::any());
     }

tool_config/kani-version.toml

@@ -2,4 +2,4 @@
 # incompatible with the verify-std repo.
 
 [kani]
-commit = "2565ef65767a696f1d519b42621b4e502e8970d0"
+commit = "8400296f5280be4f99820129bc66447e8dff63f4"