From 47f927dac1a27689d48fcafdafeed25d2c285829 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Fri, 8 Nov 2024 01:17:23 -0600
Subject: [PATCH] Update kani version

---
 library/alloc/src/lib.rs      | 1 -
 library/core/src/lib.rs       | 1 +
 library/core/src/ptr/mod.rs   | 5 ++---
 scripts/run-kani.sh           | 2 +-
 tool_config/kani-version.toml | 2 +-
 5 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs
index ffe439727719c..d28c5a29df2b9 100644
--- a/library/alloc/src/lib.rs
+++ b/library/alloc/src/lib.rs
@@ -193,7 +193,6 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
-#![cfg_attr(kani, feature(proc_macro_hygiene))]
 #![rustc_preserve_ub_checks]
 // tidy-alphabetical-end
 //
diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs
index 402c1e05b4400..42e14f7cee16e 100644
--- a/library/core/src/lib.rs
+++ b/library/core/src/lib.rs
@@ -246,6 +246,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
+#![feature(proc_macro_hygiene)]
 // tidy-alphabetical-end
 //
 // Target features:
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 46ea621b961f5..e7318fbbc6fd1 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -2626,7 +2626,7 @@ mod verify {
     }
 
     #[kani::proof]
-    pub fn check_swap_nonoverlapping_simple_untyped() {
+    pub fn check_swap_nonoverlapping_simple_untyped_slice_ptr() {
         const ARR_SIZE: usize = (2 << 32) -1;
         let mut x: [u8; ARR_SIZE] = kani::any();
         let mut xs = kani::slice::any_slice_of_array_mut(&mut x);
@@ -2636,6 +2636,5 @@ mod verify {
         unsafe {
             swap_nonoverlapping_simple_untyped(xs.as_mut_ptr(), ys.as_mut_ptr(), s);
         }
-}
-
+    }
 }
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 8ce27dac5d207..1c62a05969e34 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -183,7 +183,7 @@ main() {
 
     echo "Running Kani verify-std command..."
 
-    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
+    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12
 }
 
 main
diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml
index 5c0b4c857b6b0..c28d156262481 100644
--- a/tool_config/kani-version.toml
+++ b/tool_config/kani-version.toml
@@ -2,4 +2,4 @@
 # incompatible with the verify-std repo.
 
 [kani]
-commit = "5f8f513d297827cfdce4c48065e51973ba563068"
+commit = "8400296f5280be4f99820129bc66447e8dff63f4"