Unexpected behavior for verify-std when run inside library directory

[zhassan-aws]

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.

[celinval]

Interesting.. the Cargo.toml inside library was added fairly recently, and it is interacting in unexpected ways with kani verify-std.