Update to Rust edition 2024 and toolchain to 2025-07-03

tautschnig · tautschnig · commit fcb93f9674a8 · 2025-07-03T11:52:44.000Z
Upstream change rust-lang/rust#143214 (Remove let_chains unstable feature) requires us to either remove the use of `let` in several places or wholesale update to Rust edition 2024. Doing this edition update seems worthwhile to keep accessing more recent features, but required code changes in several places. Resolves: model-checking#4196
diff --git a/Cargo.toml b/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani-verifier"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
 keywords = ["model-checking", "verification"]
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "cprover_bindings"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
@@ -1131,7 +1131,7 @@ impl Type {
         let concrete = self.unwrap_typedef();
         match concrete {
             CInteger(CIntType::SizeT) => Some(CInteger(CIntType::SSizeT)),
-            Unsignedbv { ref width } => Some(Signedbv { width: *width }),
+            Unsignedbv { width } => Some(Signedbv { width: *width }),
             CInteger(CIntType::SSizeT) | Signedbv { .. } => Some(self.clone()),
             _ => None,
         }
@@ -1144,7 +1144,7 @@ impl Type {
         let concrete = self.unwrap_typedef();
         match concrete {
             CInteger(CIntType::SSizeT) => Some(CInteger(CIntType::SizeT)),
-            Signedbv { ref width } => Some(Unsignedbv { width: *width }),
+            Signedbv { width } => Some(Unsignedbv { width: *width }),
             CInteger(CIntType::SizeT) | Unsignedbv { .. } => Some(self.clone()),
             _ => None,
         }
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani-compiler"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -651,7 +651,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Ensure that the given instance is in the symbol table, returning the symbol.
     fn codegen_func_symbol(&mut self, instance: Instance) -> &Symbol {
-        let sym = if instance.is_foreign_item() && !instance.has_body() {
+        if instance.is_foreign_item() && !instance.has_body() {
             // Get the symbol that represents a foreign instance.
             self.codegen_foreign_fn(instance)
         } else {
@@ -661,8 +661,7 @@ impl<'tcx> GotocCtx<'tcx> {
             self.symbol_table
                 .lookup(&func)
                 .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage"))
-        };
-        sym
+        }
     }
 
     /// Generate a goto expression that references the function identified by `instance`.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -857,7 +857,7 @@ impl GotocCtx<'_> {
                     NullOp::ContractChecks | NullOp::UbChecks => Expr::c_false(),
                 }
             }
-            Rvalue::ShallowInitBox(ref operand, content_ty) => {
+            Rvalue::ShallowInitBox(operand, content_ty) => {
                 // The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box<T>.
                 // See https://github.com/rust-lang/compiler-team/issues/460 for more details.
                 let operand = self.codegen_operand_stable(operand);
@@ -947,7 +947,7 @@ impl GotocCtx<'_> {
                 let pt = self.place_ty_stable(p);
                 self.codegen_get_discriminant(place, pt, res_ty)
             }
-            Rvalue::Aggregate(ref k, operands) => {
+            Rvalue::Aggregate(k, operands) => {
                 self.codegen_rvalue_aggregate(k, operands, res_ty, loc)
             }
             Rvalue::ThreadLocalRef(def_id) => {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -216,7 +216,7 @@ impl GotocCtx<'_> {
             // https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.NonDivergingIntrinsic.html#variant.Assume
             // Informs the optimizer that a condition is always true.
             // If the condition is false, the behavior is undefined.
-            StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(ref op)) => {
+            StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(op)) => {
                 let cond = self.codegen_operand_stable(op).cast_to(Type::bool());
                 self.codegen_assert_assume(
                     cond,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1754,7 +1754,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &self,
         instance: InstanceStable,
         fn_abi: &'a FnAbi,
-    ) -> impl Iterator<Item = (usize, &'a ArgAbi)> {
+    ) -> impl Iterator<Item = (usize, &'a ArgAbi)> + use<'a> {
         let requires_caller_location = self.requires_caller_location(instance);
         let num_args = fn_abi.args.len();
         fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -451,7 +451,7 @@ impl GotocCtx<'_> {
     ) -> Stmt {
         match stmt.body() {
             StmtBody::Return(Some(expr)) => {
-                if let ExprValue::Symbol { ref identifier } = expr.value() {
+                if let ExprValue::Symbol { identifier } = expr.value() {
                     *return_symbol = Some(Expr::symbol_expression(*identifier, expr.typ().clone()));
                     Stmt::goto(*end_label, *stmt.location())
                 } else {
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
@@ -150,7 +150,7 @@ fn resolve_path<'tcx>(
     path.segments.into_iter().try_fold(path.base, |base, segment| {
         let name = segment.ident.to_string();
         let def_kind = tcx.def_kind(base);
-        let next_item = match def_kind {
+        match def_kind {
             DefKind::ForeignMod | DefKind::Mod => resolve_in_module(tcx, base, &name),
             DefKind::Struct | DefKind::Enum | DefKind::Union => {
                 resolve_in_type_def(tcx, base, &path.base_path_args, &name)
@@ -160,8 +160,7 @@ fn resolve_path<'tcx>(
                 debug!(?base, ?kind, "resolve_path: unexpected item");
                 Err(ResolveError::UnexpectedType { tcx, item: base, expected: "module" })
             }
-        };
-        next_item
+        }
     })
 }
 
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -88,9 +88,7 @@ impl AnyModifiesPass {
         let kani_write_any_str = kani_fns.get(&KaniModel::WriteAnyStr.into()).copied();
         let target_fn = if let Some(harness) = unit.harnesses.first() {
             let attributes = KaniAttributes::for_instance(tcx, *harness);
-            let target_fn =
-                attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern());
-            target_fn
+            attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern())
         } else {
             None
         };
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani-driver"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
 homepage = "https://github.com/model-checking/kani"
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani_metadata"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs
@@ -42,7 +42,7 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
 
 /// Iterate over `any_raw_internal` since CBMC produces assignment per element.
 pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
-    [(); N].map(|_| crate::any_raw_internal::<T>())
+    unsafe { [(); N].map(|_| crate::any_raw_internal::<T>()) }
 }
 
 /// Concrete playback implementation of
diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs
@@ -189,9 +189,11 @@ mod intrinsics {
             "Expected size of input and lanes to match",
         );
 
-        let data = &*(&input as *const T as *const [E; LANES]);
-        let mask = simd_bitmask_impl(data);
-        (&mask as *const [u8; mask_len(LANES)] as *const U).read()
+        unsafe {
+            let data = &*(&input as *const T as *const [E; LANES]);
+            let mask = simd_bitmask_impl(data);
+            (&mask as *const [u8; mask_len(LANES)] as *const U).read()
+        }
     }
 
     /// Structure used for sanity check our parameters.
diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani_core"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 description = "Define core constructs to use with Kani"
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani_macros"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
@@ -155,7 +155,7 @@ fn field_refs(ident: &Ident, data: &Data) -> TokenStream {
 /// references to the struct fields. See `field_refs` for more details.
 fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             let field_refs: Vec<TokenStream> = fields
                 .named
                 .iter()
@@ -187,7 +187,7 @@ fn safe_body_default(ident: &Ident, data: &Data) -> TokenStream {
 
 fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             let field_safe_calls: Vec<TokenStream> = fields
                 .named
                 .iter()
@@ -204,7 +204,7 @@ fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
                 quote! { true }
             }
         }
-        Fields::Unnamed(ref fields) => {
+        Fields::Unnamed(fields) => {
             let field_safe_calls: Vec<TokenStream> = fields
                 .unnamed
                 .iter()
@@ -232,7 +232,7 @@ fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
 /// For unit field, generate an empty initialization.
 fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             // Use the span of each `syn::Field`. This way if one of the field types does not
             // implement `Arbitrary` then the compiler's error message underlines which field it
             // is. An example is shown in the readme of the parent directory.
@@ -246,7 +246,7 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
                 #ident {#( #init,)*}
             }
         }
-        Fields::Unnamed(ref fields) => {
+        Fields::Unnamed(fields) => {
             // Expands to an expression like
             // Self(kani::any(), kani::any(), ..., kani::any());
             let init = fields.unnamed.iter().map(|field| {
@@ -490,7 +490,7 @@ fn has_field_safety_constraints(ident: &Ident, data: &Data) -> bool {
 /// field.
 fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool {
     match fields {
-        Fields::Named(ref fields) => fields
+        Fields::Named(fields) => fields
             .named
             .iter()
             .any(|field| field.attrs.iter().any(|attr| attr.path().is_ident("safety_constraint"))),
@@ -570,7 +570,7 @@ fn safe_body_from_fields_attr_inner(ident: &Ident, fields: &Fields) -> TokenStre
         // Expands to the expression
         // `<safety_cond1> && <safety_cond2> && ..`
         // where `<safety_condN>` is the safety condition specified for the N-th field.
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             let safety_conds: Vec<TokenStream> =
                 fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect();
             quote! { #(#safety_conds)&&* }
diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -114,7 +114,7 @@ impl<'a> ContractConditionsHandler<'a> {
         replace_closure: &TokenStream,
         check_closure: &TokenStream,
     ) -> TokenStream {
-        let ItemFn { ref sig, .. } = self.annotated_fn;
+        let ItemFn { sig, .. } = self.annotated_fn;
         let output = &sig.output;
         let span = Span::call_site();
         let result = Ident::new(INTERNAL_RESULT_IDENT, span);
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -189,7 +189,7 @@ impl<T: OldTrigger> syn::visit_mut::VisitMut for OldVisitor<'_, T> {
         };
         if trigger {
             let span = ex.span();
-            let new_expr = if let Expr::Call(ExprCall { ref mut args, .. }) = ex {
+            let new_expr = if let Expr::Call(ExprCall { args, .. }) = ex {
                 self.t
                     .trigger(args.iter_mut().next().unwrap(), span, self.remembers_exprs)
                     .then(|| args.pop().unwrap().into_value())
diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs
@@ -226,7 +226,7 @@ fn transform_break_continue(block: &mut Block) {
         return (true, None);
     };
     // Add semicolon to the last statement if it's an expression without semicolon
-    if let Some(Stmt::Expr(_, ref mut semi)) = block.stmts.last_mut() {
+    if let Some(&mut Stmt::Expr(_, ref mut semi)) = block.stmts.last_mut() {
         if semi.is_none() {
             *semi = Some(Default::default());
         }
@@ -300,9 +300,9 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
     register_name.push_str(&loop_id);
     let register_ident = format_ident!("{}", register_name);
 
-    match loop_stmt {
-        Stmt::Expr(ref mut e, _) => match e {
-            Expr::While(ref mut ew) => {
+    match &mut loop_stmt {
+        &mut Stmt::Expr(ref mut e, _) => match e {
+            &mut Expr::While(ref mut ew) => {
                 let new_cond: Expr = syn::parse(
                     quote!(
                         #register_ident(&||->bool{#inv_expr}, 0))
@@ -316,7 +316,7 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
                     right: ew.cond.clone(),
                 });
             }
-            Expr::Loop(ref mut el) => {
+            &mut Expr::Loop(ref mut el) => {
                 //let retexpr = get_return_statement(&el.body);
                 let invstmt: Stmt = syn::parse(quote!(if !(#register_ident(&||->bool{#inv_expr}, 0)) {assert!(false); unreachable!()};).into()).unwrap();
                 let mut new_stmts: Vec<Stmt> = Vec::new();
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
@@ -6,7 +6,7 @@
 # standard library symbols are preserved
 name = "std"
 version = "0.63.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-07-02"
+channel = "nightly-2025-07-03"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/rustfmt.toml b/rustfmt.toml
@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 # Run rustfmt with this config (it should be picked up automatically).
-edition = "2021"
+edition = "2024"
 style_edition = "2024"
 use_small_heuristics = "Max"
 merge_derives = false
diff --git a/src/lib.rs b/src/lib.rs
@@ -115,15 +115,14 @@ fn parse_args(args: Vec<OsString>) -> ArgsResult {
 /// hundreds of HTTP requests trying to download a non-existent release bundle.
 /// So if we positively detect a dev environment, raise an error early.
 fn fail_if_in_dev_environment() -> Result<()> {
-    if let Ok(exe) = std::env::current_exe() {
-        if let Some(path) = exe.parent() {
-            if path.ends_with("target/debug") || path.ends_with("target/release") {
-                bail!(
-                    "Running a release-only executable, {}, from a development environment. This is usually caused by PATH including 'target/release' erroneously.",
-                    exe.file_name().unwrap().to_string_lossy()
-                )
-            }
-        }
+    if let Ok(exe) = std::env::current_exe()
+        && let Some(path) = exe.parent()
+        && (path.ends_with("target/debug") || path.ends_with("target/release"))
+    {
+        bail!(
+            "Running a release-only executable, {}, from a development environment. This is usually caused by PATH including 'target/release' erroneously.",
+            exe.file_name().unwrap().to_string_lossy()
+        )
     }
 
     Ok(())
@@ -194,7 +193,9 @@ fn fixup_dynamic_linking_environment() {
         // unwrap safety: we're just filtering, so it should always succeed
         let new_val =
             env::join_paths(env::split_paths(&paths).filter(unlike_toolchain_path)).unwrap();
-        env::set_var(LOADER_PATH, new_val);
+        unsafe {
+            env::set_var(LOADER_PATH, new_val);
+        }
     }
 }
 
@@ -217,7 +218,9 @@ fn unlike_toolchain_path(path: &PathBuf) -> bool {
 /// down to children) with the toolchain Kani uses instead.
 fn set_kani_rust_toolchain(kani_dir: &Path) -> Result<()> {
     let toolchain_verison = setup::get_rust_toolchain_version(kani_dir)?;
-    env::set_var("RUSTUP_TOOLCHAIN", toolchain_verison);
+    unsafe {
+        env::set_var("RUSTUP_TOOLCHAIN", toolchain_verison);
+    }
     Ok(())
 }
 
diff --git a/src/setup.rs b/src/setup.rs
diff --git a/tests/kani/Coroutines/issue-1593.rs b/tests/kani/Coroutines/issue-1593.rs
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
diff --git a/tools/compiletest/Cargo.toml b/tools/compiletest/Cargo.toml
diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs
diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml
diff --git a/tools/scanner/Cargo.toml b/tools/scanner/Cargo.toml
diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs

Original file line number	Diff line number	Diff line change
`@@ -857,7 +857,7 @@ impl GotocCtx<'_> {`
`857`	`857`	`NullOp::ContractChecks \| NullOp::UbChecks => Expr::c_false(),`
`858`	`858`	`}`
`859`	`859`	`}`
`860`		`- Rvalue::ShallowInitBox(ref operand, content_ty) => {`
	`860`	`+ Rvalue::ShallowInitBox(operand, content_ty) => {`
`861`	`861`	`// The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box<T>.`
`862`	`862`	`// See https://github.com/rust-lang/compiler-team/issues/460 for more details.`
`863`	`863`	`let operand = self.codegen_operand_stable(operand);`
`@@ -947,7 +947,7 @@ impl GotocCtx<'_> {`
`947`	`947`	`let pt = self.place_ty_stable(p);`
`948`	`948`	`self.codegen_get_discriminant(place, pt, res_ty)`
`949`	`949`	`}`
`950`		`- Rvalue::Aggregate(ref k, operands) => {`
	`950`	`+ Rvalue::Aggregate(k, operands) => {`
`951`	`951`	`self.codegen_rvalue_aggregate(k, operands, res_ty, loc)`
`952`	`952`	`}`
`953`	`953`	`Rvalue::ThreadLocalRef(def_id) => {`