Ensure storage markers are kept in std code

model-checking · Mar 14, 2024 · fc512ac · fc512ac
1 parent a52564d
commit fc512ac
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
@@ -123,7 +123,7 @@ impl KaniSession {
  "-Z",
  "panic_abort_tests=yes",
  "-Z",
- "sanitizer=address",
+ "mir-enable-passes=-RemoveStorageMarkers",
  ]
  .map(OsString::from),
  );

diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs
@@ -124,7 +124,14 @@ fn build_kani_lib(
  "--message-format",
  "json-diagnostic-rendered-ansi",
  ];
- let mut rustc_args = vec!["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"];
+ let mut rustc_args = vec![
+ "--cfg=kani",
+ "--cfg=kani_sysroot",
+ "-Z",
+ "always-encode-mir",
+ "-Z",
+ "mir-enable-passes=-RemoveStorageMarkers",
+ ];
  rustc_args.extend_from_slice(extra_rustc_args);
  let mut cmd = Command::new("cargo")
  .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join("\x1f"))