From fd015575500bead70e3303f3563e44f53eed3adf Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 7 Oct 2024 15:03:58 -0700
Subject: [PATCH] Add test

---
 .../verify_std_cmd/verify_std.expected        |  4 ++
 .../verify_std_cmd/verify_std.sh              | 39 ++++++++++++++++---
 2 files changed, 37 insertions(+), 6 deletions(-)

diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected
index 157adb94ba16..3c1f474af0e7 100644
--- a/tests/script-based-pre/verify_std_cmd/verify_std.expected
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected
@@ -1,3 +1,7 @@
+[TEST] Only codegen inside library folder
+No kani crate inside Cargo.toml as expected
+
+
 [TEST] Run kani verify-std
 
 Checking harness verify::dummy_proof...
diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh
index 022e7b79de4a..e7276867a2a5 100755
--- a/tests/script-based-pre/verify_std_cmd/verify_std.sh
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh
@@ -50,17 +50,44 @@ cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs
 echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs
 cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs
 
+# Test that the command works inside the library folder and does not change
+# the existing workspace
+# See https://github.com/model-checking/kani/issues/3574
+echo "[TEST] Only codegen inside library folder"
+pushd "${TMP_DIR}/library" >& /dev/null
+RUSTFLAGS="--cfg=uninit_checks" kani verify-std \
+    -Z unstable-options \
+    . \
+    -Z function-contracts \
+    -Z stubbing \
+    -Z mem-predicates \
+    --only-codegen
+popd
+# Grep should not find anything and exit status is 1.
+grep -c kani ${TMP_DIR}/library/Cargo.toml \
+    && echo "Unexpected kani crate inside Cargo.toml" \
+    || echo "No kani crate inside Cargo.toml as expected"
+
 echo "[TEST] Run kani verify-std"
 export RUST_BACKTRACE=1
-kani verify-std -Z unstable-options "${TMP_DIR}/library" \
-    --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \
+kani verify-std \
+    -Z unstable-options \
+    "${TMP_DIR}/library" \
+    --target-dir "${TMP_DIR}/target" \
+    -Z function-contracts \
+    -Z stubbing \
     -Z mem-predicates
 
+# Test that uninit-checks basic setup works on a no-core library
 echo "[TEST] Run kani verify-std -Z uninit-checks"
-export RUSTFLAGS="--cfg=uninit_checks"
-kani verify-std -Z unstable-options "${TMP_DIR}/library" \
-    --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \
-    -Z mem-predicates -Z uninit-checks
+RUSTFLAGS="--cfg=uninit_checks" kani verify-std \
+    -Z unstable-options \
+    "${TMP_DIR}/library" \
+    --target-dir "${TMP_DIR}/target" \
+    -Z function-contracts \
+    -Z stubbing \
+    -Z mem-predicates \
+    -Z uninit-checks
 
 # Cleanup
 rm -r ${TMP_DIR}