From 72160bc9a8286320eb46caad841eb32144ce10b1 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 26 Jul 2024 21:35:55 +0000
Subject: [PATCH] check with updated scripts with local paths

---
 scripts/check-kani.sh | 47 ++++++++++++++++++++++---------------------
 1 file changed, 24 insertions(+), 23 deletions(-)

diff --git a/scripts/check-kani.sh b/scripts/check-kani.sh
index e250c62b7df3f..987f614dddca4 100755
--- a/scripts/check-kani.sh
+++ b/scripts/check-kani.sh
@@ -4,34 +4,35 @@
 VERIFY_RUST_STD_DIR="/tmp/verify-rust-std"
 KANI_DIR="/tmp/kani"
 
-# Checkout your local repository
-echo "Checking out local repository..."
-echo
-cd "$VERIFY_RUST_STD_DIR"
-
-# Checkout the Kani repository
-echo "Checking out Kani repository..."
-echo
-git clone --depth 1 -b features/verify-rust-std https://github.com/model-checking/kani.git "$KANI_DIR"
-
-# Setup dependencies for Kani
-echo "Setting up dependencies for Kani..."
-echo
-cd "$KANI_DIR"
-./scripts/setup/ubuntu/install_deps.sh
-
-# Build Kani
-echo "Building Kani..."
-echo
-cargo build-dev --release
-echo "$(pwd)/scripts" >> $PATH
+RUNNER_TEMP=$(mktemp -d)
+
+# # Checkout your local repository
+# echo "Checking out local repository..."
+# echo
+# cd "$VERIFY_RUST_STD_DIR"
+
+# # Checkout the Kani repository
+# echo "Checking out Kani repository..."
+# echo
+# git clone --depth 1 -b features/verify-rust-std https://github.com/model-checking/kani.git "$KANI_DIR"
+
+# # Setup dependencies for Kani
+# echo "Setting up dependencies for Kani..."
+# echo
+# cd "$KANI_DIR"
+# ./scripts/setup/ubuntu/install_deps.sh
+
+# # Build Kani
+# echo "Building Kani..."
+# echo
+# cargo build-dev --release
+# echo "$(pwd)/scripts" >> $PATH
 
 # Run tests
 echo "Running tests..."
 echo
 cd "$VERIFY_RUST_STD_DIR"
-kani verify-std -Z unstable-options ./library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates -Z ptr-to-ref-cast-checks
-RUST_BACKTRACE=1
+/tmp/kani/scripts/kani verify-std -Z unstable-options /tmp/verify-rust-std/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates -Z ptr-to-ref-cast-checks
 
 echo "Tests completed."
 echo