Upgrade toolchain to 2025-03-18

kani-compiler/src/kani_compiler.rs

@@ -41,6 +41,7 @@ pub fn run(args: Vec<String>) {
 }
 
 /// Configure the LLBC backend (Aeneas's IR).
+#[allow(unused)]
 fn llbc_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
     #[cfg(feature = "llbc")]
     return Box::new(LlbcCodegenBackend::new(_queries));
@@ -49,6 +50,7 @@ fn llbc_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
 }
 
 /// Configure the cprover backend that generates goto-programs.
+#[allow(unused)]
 fn cprover_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
     #[cfg(feature = "cprover")]
     return Box::new(GotocCodegenBackend::new(_queries));

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-03-17"
+channel = "nightly-2025-03-18"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

scripts/kani-regression.sh

@@ -105,7 +105,12 @@ cargo clean --manifest-path "$FEATURES_MANIFEST_PATH"
 # Setting RUSTFLAGS like this always resets cargo's build cache resulting in
 # all tests to be re-run. I.e., cannot keep re-runing the regression from where
 # we stopped.
-RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings
+# Only run with the `cprover` feature to avoid compiling the `charon` library
+# which is not our code and may have warnings. The downside is that we wouldn't
+# detect any warnings in the charon code path. TODO: Remove
+# `--no-default-features --features cprover` when the warnings in charon are
+# fixed and we advance the charon pin to that version
+RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings --no-default-features --features cprover
 
 echo
 echo "All Kani regression tests completed successfully."