cargo-creusot: Disable incremental compilation

creusot-rs · Dec 4, 2024 · 0c275ae · 0c275ae
1 parent 7f18d4f
commit 0c275ae
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 19 deletions.
diff --git a/cargo-creusot/src/main.rs b/cargo-creusot/src/main.rs
@@ -137,6 +137,9 @@ fn invoke_cargo(args: &CreusotArgs, cargo_flags: Vec<String>) {
         .args(cargo_flags)
         .env("RUSTC", creusot_rustc_path)
         .env("CARGO_CREUSOT", "1");
+    // Incremental compilation causes Creusot to not see all of a crate's code
+    // (the `mir_borrowck` hook in `creusot/src/callbacks.rs` is not called on all closures).
+    cmd.env("CARGO_INCREMENTAL", "0");
 
     // Append flags to any pre-existing ones
     // CARGO_ENCODED_RUSTFLAGS contains options to pass to rustc, separated by '\x1f'.

diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma