Upgrade toolchain to 2025-03-18 (#3959)

The main change to get the toolchain upgrade to 2025-03-18 to work is to
make this change in `kani-regression.sh`:
```diff
-RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings
+RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings --no-default-features --features cprover
```
Explanation:
1. `cargo build` suppresses warnings from dependencies unless they're
local dependencies (e.g. included with `path = ...`) (see
rust-lang/cargo#8546)
2. Since we integrate `charon` as a git submodule and add it as a
dependency using `path = ...`, its warnings are not suppressed
3. The toolchain upgrade includes adding a `#[must_use]` attribute on an
enum used in charon:
rust-lang/rust@2439623278. This results in a
warning that causes the `RUSTFLAGS="-D warnings" cargo build` to fail:
https://github.com/model-checking/kani/actions/runs/13914318184/job/38934470822#step:4:2983

The short-term solution in this PR is to exclude the Charon feature when
building with `-D warnings`.

The long-term solution is to fix the warning in upstream Charon (if it's
not already fixed), and update our Charon pin to point to a commit that
includes the fix. Updating the Charon pin requires us to upgrade our MIR
to ULLBC module though, which will require a non-trivial amount of work
since it's 2.5 months old.

Resolves #3944

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws

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."