diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 191b104a8c1c..bc0e9d8361d7 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -46,10 +46,39 @@ pub struct CargoOutputs { impl KaniSession { /// Create a new cargo library in the given path. + /// + /// Since we cannot create a new workspace with `cargo init --lib`, we create the dummy + /// crate manually. =( See . + /// + /// Without setting up a new workspace, cargo init will modify the workspace where this is + /// running. See for details. pub fn cargo_init_lib(&self, path: &Path) -> Result<()> { - let mut cmd = setup_cargo_command()?; - cmd.args(["init", "--lib", path.to_string_lossy().as_ref()]); - self.run_terminal(cmd) + let toml_path = path.join("Cargo.toml"); + if toml_path.exists() { + bail!("Cargo.toml already exists in {}", path.display()); + } + + // Create folder for library + fs::create_dir_all(path.join("src"))?; + + // Create dummy crate and write dummy body + let lib_path = path.join("src/lib.rs"); + fs::write(&lib_path, "pub fn dummy() {}")?; + + // Create Cargo.toml + fs::write( + &toml_path, + r#"[package] +name = "dummy" +version = "0.1.0" + +[lib] +crate-type = ["lib"] + +[workspace] +"#, + )?; + Ok(()) } pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result> { 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}