Update to Rust edition 2024

Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "kani-verifier"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
 keywords = ["model-checking", "verification"]

cprover_bindings/Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "cprover_bindings"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 

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,
         }

kani-compiler/Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "kani-compiler"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 

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

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) => {

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,

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)| {

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 {

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
+        }
     })
 }
 

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
         };

kani-driver/Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "kani-driver"
 version = "0.64.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"

kani_metadata/Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "kani_metadata"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 

library/kani/Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "kani"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 

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

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.

library/kani_core/Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "kani_core"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 description = "Define core constructs to use with Kani"

library/kani_macros/Cargo.toml

@@ -4,7 +4,7 @@
 [package]
 name = "kani_macros"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 

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)&&* }

library/kani_macros/src/sysroot/contracts/bootstrap.rs

@@ -128,7 +128,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);

library/kani_macros/src/sysroot/contracts/initialize.rs

@@ -19,10 +19,10 @@ impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState {
     /// Find out if this attribute could be describing a "contract handling"
     /// state and if so return it.
     fn try_from(attribute: &'a syn::Attribute) -> Result<Self, Self::Error> {
-        if let syn::Meta::NameValue(nv) = &attribute.meta {
-            if matches_path(&nv.path, &["kanitool", "checked_with"]) {
-                return Ok(ContractFunctionState::Expanded);
-            }
+        if let syn::Meta::NameValue(nv) = &attribute.meta
+            && matches_path(&nv.path, &["kanitool", "checked_with"])
+        {
+            return Ok(ContractFunctionState::Expanded);
         }
         Err(None)
     }

library/kani_macros/src/sysroot/contracts/shared.rs

@@ -51,14 +51,14 @@ pub fn split_for_remembers(stmts: &[Stmt], contract_mode: ContractMode) -> (&[St
     };
 
     for stmt in stmts {
-        if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt {
-            if let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref() {
-                let first_two_idents =
-                    segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
-
-                if first_two_idents == vec!["kani", check_str] {
-                    pos += 1;
-                }
+        if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt
+            && let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref()
+        {
+            let first_two_idents =
+                segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
+
+            if first_two_idents == vec!["kani", check_str] {
+                pos += 1;
             }
         }
     }
@@ -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())

library/kani_macros/src/sysroot/loop_contracts/mod.rs

@@ -137,20 +137,18 @@ impl VisitMut for CallReplacer {
         // Visit nested expressions first
         syn::visit_mut::visit_expr_mut(self, expr);
 
-        if let Expr::Call(call) = expr {
-            if let Expr::Path(expr_path) = &*call.func {
-                if self.should_replace(expr_path) {
-                    let replace_var =
-                        self.replacements.iter().find(|(e, _)| e == expr).map(|(_, v)| v);
-                    if let Some(var) = replace_var {
-                        *expr = syn::parse_quote!(#var);
-                    } else {
-                        let new_var = self.generate_var_name();
-                        self.replacements.push((expr.clone(), new_var.clone()));
-                        *expr = syn::parse_quote!(#new_var);
-                    };
-                }
-            }
+        if let Expr::Call(call) = expr
+            && let Expr::Path(expr_path) = &*call.func
+            && self.should_replace(expr_path)
+        {
+            let replace_var = self.replacements.iter().find(|(e, _)| e == expr).map(|(_, v)| v);
+            if let Some(var) = replace_var {
+                *expr = syn::parse_quote!(#var);
+            } else {
+                let new_var = self.generate_var_name();
+                self.replacements.push((expr.clone(), new_var.clone()));
+                *expr = syn::parse_quote!(#new_var);
+            };
         }
     }
 }
@@ -226,10 +224,10 @@ 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 semi.is_none() {
-            *semi = Some(Default::default());
-        }
+    if let Some(&mut Stmt::Expr(_, ref mut semi)) = block.stmts.last_mut()
+        && semi.is_none()
+    {
+        *semi = Some(Default::default());
     }
     block.stmts.push(return_stmt);
 }
@@ -300,8 +298,8 @@ 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 {
+    match &mut loop_stmt {
+        &mut Stmt::Expr(ref mut e, _) => match *e {
             Expr::While(ref mut ew) => {
                 let new_cond: Expr = syn::parse(
                     quote!(

library/std/Cargo.toml

@@ -6,7 +6,7 @@
 # standard library symbols are preserved
 name = "std"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false