Closed
Description
This issue was pointed out by @QinyuanWu in model-checking/verify-rust-std#98.
When the kani verify-std command is run inside the library directory of the verify-rust-std repository, it causes the Cargo.toml and Cargo.lock files to change:
$ pwd
/home/ubuntu/git/verify-rust-std/library
$ kani verify-std -Zunstable-options . -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify
Kani Rust Verifier 0.55.0 (standalone)
Creating library package
Adding `kani_verify_std` as member of workspace at `/home/zyadh/git/verify-rust-std/library`
note: see more `Cargo.toml` keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
Updating crates.io index
Locking 8 packages to latest compatible versions
Adding proc-macro-error v1.0.4
Adding proc-macro-error-attr v1.0.4
Adding proc-macro2 v1.0.87
Adding quote v1.0.37
Adding syn v1.0.109 (latest: v2.0.79)
Adding syn v2.0.79
Adding unicode-ident v1.0.13
Adding version_check v0.9.5
Compiling proc-macro2 v1.0.87
Compiling version_check v0.9.5
Compiling unicode-ident v1.0.13
Compiling syn v1.0.109
Compiling safety v0.1.0 (/home/zyadh/git/verify-rust-std/library/contracts/safety)
Compiling compiler_builtins v0.1.123
Compiling libc v0.2.158
Compiling memchr v2.5.0
...$ git diff Cargo.toml
diff --git a/library/Cargo.toml b/library/Cargo.toml
index e744cfe5e0f..b60256ed7a8 100644
--- a/library/Cargo.toml
+++ b/library/Cargo.toml
@@ -2,7 +2,7 @@
resolver = "1"
members = [
"std",
- "sysroot",
+ "sysroot", "target/kani_verify_std",
]
exclude = [
In addition, unless one runs cargo clean, any modifications to the source code will not be taken into account for the next kani verify-std run (i.e., apparently the command will run on a cached version of the library).
The solution is to run Kani outside of this directory, e.g. in the root directory of verify-rust-std.