diff --git a/Cargo.toml b/Cargo.toml index f44b3c230ddf..692a978c5fec 100644 --- a/Cargo.toml +++ b/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"] diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index a034eb188170..34ccee41c4f7 100644 --- a/cprover_bindings/Cargo.toml +++ b/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 diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index bf4479410821..01148089e7d5 100644 --- 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 index b2975aeda5d2..8e575dd5941b 100644 --- a/kani-compiler/Cargo.toml +++ b/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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 0cfa0e6c1352..9cafc55b3974 100644 --- 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 index 05995ca4bb71..31f8da6f32a4 100644 --- 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. // 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 index 1fbd208bfc03..e740cdf3ab96 100644 --- 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 index 5554458e7589..d950d4262300 100644 --- 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 { + ) -> impl Iterator + 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 index 879dd24870ee..ee92db922527 100644 --- 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 index 865a96d408e4..b19f2da89d83 100644 --- 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 index e3ca9a53c66b..c34d145790d1 100644 --- 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 index c07841ac0dd0..2ea7e08c7141 100644 --- a/kani-driver/Cargo.toml +++ b/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" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 43b5cbcadc98..bb3b99c4a8c9 100644 --- a/kani_metadata/Cargo.toml +++ b/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 diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index aa97b03376cd..2a25cf3a43fa 100644 --- a/library/kani/Cargo.toml +++ b/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 diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs index 0de51862b7d8..cba6c000562f 100644 --- a/library/kani/src/concrete_playback.rs +++ b/library/kani/src/concrete_playback.rs @@ -42,7 +42,7 @@ pub fn concrete_playback_run(mut local_concrete_vals: Vec>, pro /// Iterate over `any_raw_internal` since CBMC produces assignment per element. pub(crate) unsafe fn any_raw_array() -> [T; N] { - [(); N].map(|_| crate::any_raw_internal::()) + unsafe { [(); N].map(|_| crate::any_raw_internal::()) } } /// Concrete playback implementation of diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index ecd3646b5b3a..e11e15e4f709 100644 --- 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 index 4aa954b8994d..f98dcfec355e 100644 --- a/library/kani_core/Cargo.toml +++ b/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" diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 90abc11ad0ab..c6c8291a6591 100644 --- a/library/kani_macros/Cargo.toml +++ b/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 diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index cfc3b1df8fc9..388dd64057b1 100644 --- 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 = 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 = 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 = 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 // ` && && ..` // where `` is the safety condition specified for the N-th field. - Fields::Named(ref fields) => { + Fields::Named(fields) => { let safety_conds: Vec = 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 index 1e8efdf04eb0..ed8bde7f8974 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/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); diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index 2d2e2d28b190..ac9ab7252562 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/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 { - 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) } diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 816a3623f6b2..51547ea55a98 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/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::>(); - - 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::>(); + + if first_two_idents == vec!["kani", check_str] { + pos += 1; } } } @@ -189,7 +189,7 @@ impl 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 index fc129c6d92bc..7f8577694a8f 100644 --- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs +++ b/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!( diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index c9af45468c66..fe3670b6b0fa 100644 --- a/library/std/Cargo.toml +++ b/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 diff --git a/rustfmt.toml b/rustfmt.toml index f8ff0d0fd105..d77b82e0cf51 100644 --- 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 index 5b79ec504d4c..4f999a868f9f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -115,6 +115,9 @@ fn parse_args(args: Vec) -> 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<()> { + // Don't collapse if as let_chains have only been stabilized in 1.88, which the target host + // installing Kani need not have just yet. + #[allow(clippy::collapsible_if)] 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") { @@ -194,7 +197,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 +222,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 index 96daf82e4a27..b33e69b15ec9 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -60,6 +60,9 @@ pub fn appears_incomplete() -> Option { let kani_dir_parent = kani_dir.parent().unwrap(); for entry in std::fs::read_dir(kani_dir_parent).ok()?.flatten() { + // Don't collapse if as let_chains have only been stabilized in 1.88, which the target host + // installing Kani need not have just yet. + #[allow(clippy::collapsible_if)] if let Some(file_name) = entry.file_name().to_str() { if file_name.ends_with(".tar.gz") { return Some(kani_dir_parent.join(file_name)); diff --git a/tests/kani/Coroutines/issue-1593.rs b/tests/kani/Coroutines/issue-1593.rs index b85aefba9378..989f91c4f346 100644 --- a/tests/kani/Coroutines/issue-1593.rs +++ b/tests/kani/Coroutines/issue-1593.rs @@ -16,10 +16,10 @@ use std::sync::{ fn issue_1593() { let x = Arc::new(AtomicI64::new(0)); let x2 = x.clone(); - let gen = async move { + let y = async move { async {}.await; x2.fetch_add(1, Ordering::Relaxed); }; - assert_eq!(std::mem::size_of_val(&gen), 16); - let pinbox = Box::pin(gen); // check that vtables work + assert_eq!(std::mem::size_of_val(&y), 16); + let pinbox = Box::pin(y); // check that vtables work } diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs index cc63b6b21186..d6b670d80112 100644 --- a/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs +++ b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs @@ -24,16 +24,16 @@ use std::pin::Pin; use std::sync::atomic::{AtomicUsize, Ordering}; fn drain + Unpin, R, Y>( - gen: &mut G, + g: &mut G, inout: Vec<(R, CoroutineState)>, ) where Y: Debug + PartialEq, G::Return: Debug + PartialEq, { - let mut gen = Pin::new(gen); + let mut g = Pin::new(g); for (input, out) in inout { - assert_eq!(gen.as_mut().resume(input), out); + assert_eq!(g.as_mut().resume(input), out); } } diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index ce1b24e93c1e..523713c2e0f6 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -4,7 +4,7 @@ [package] name = "build-kani" version = "0.64.0" -edition = "2021" +edition = "2024" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" publish = false diff --git a/tools/compiletest/Cargo.toml b/tools/compiletest/Cargo.toml index fe0a6b10df4a..4e2b80340eb3 100644 --- a/tools/compiletest/Cargo.toml +++ b/tools/compiletest/Cargo.toml @@ -6,7 +6,7 @@ [package] name = "compiletest" version = "0.0.0" -edition = "2021" +edition = "2024" license = "MIT OR Apache-2.0" publish = false # From upstream compiletest: diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 8c0a2dd0b08d..90900d0c114c 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -51,10 +51,17 @@ fn add_kani_to_path() { let cwd = env::current_dir().unwrap(); let kani_bin = cwd.join("target").join("debug"); let kani_scripts = cwd.join("scripts"); - env::set_var( - "PATH", - format!("{}:{}:{}", kani_scripts.display(), kani_bin.display(), env::var("PATH").unwrap()), - ); + unsafe { + env::set_var( + "PATH", + format!( + "{}:{}:{}", + kani_scripts.display(), + kani_bin.display(), + env::var("PATH").unwrap() + ), + ); + } } pub fn parse_config(args: Vec) -> Config { @@ -230,10 +237,14 @@ pub fn run_tests(config: Config) { } // Prevent issue #21352 UAC blocking .exe containing 'patch' etc. on Windows // If #11207 is resolved (adding manifest to .exe) this becomes unnecessary - env::set_var("__COMPAT_LAYER", "RunAsInvoker"); + unsafe { + env::set_var("__COMPAT_LAYER", "RunAsInvoker"); + } // Let tests know which target they're running as - env::set_var("TARGET", &config.target); + unsafe { + env::set_var("TARGET", &config.target); + } let opts = test_opts(&config); diff --git a/tools/compiletest/src/raise_fd_limit.rs b/tools/compiletest/src/raise_fd_limit.rs index 1359241c0cd2..438b8e9c9728 100644 --- a/tools/compiletest/src/raise_fd_limit.rs +++ b/tools/compiletest/src/raise_fd_limit.rs @@ -28,8 +28,9 @@ pub unsafe fn raise_fd_limit() { let mut mib: [libc::c_int; 2] = [CTL_KERN, KERN_MAXFILESPERPROC]; let mut maxfiles: libc::c_int = 0; let mut size: libc::size_t = size_of_val(&maxfiles) as libc::size_t; - if libc::sysctl(&mut mib[0], 2, &mut maxfiles as *mut _ as *mut _, &mut size, null_mut(), 0) - != 0 + if unsafe { + libc::sysctl(&mut mib[0], 2, &mut maxfiles as *mut _ as *mut _, &mut size, null_mut(), 0) + } != 0 { let err = io::Error::last_os_error(); panic!("raise_fd_limit: error calling sysctl: {err}"); @@ -37,7 +38,7 @@ pub unsafe fn raise_fd_limit() { // Fetch the current resource limits let mut rlim = libc::rlimit { rlim_cur: 0, rlim_max: 0 }; - if libc::getrlimit(libc::RLIMIT_NOFILE, &mut rlim) != 0 { + if unsafe { libc::getrlimit(libc::RLIMIT_NOFILE, &mut rlim) } != 0 { let err = io::Error::last_os_error(); panic!("raise_fd_limit: error calling getrlimit: {err}"); } @@ -48,7 +49,7 @@ pub unsafe fn raise_fd_limit() { rlim.rlim_cur = cmp::min(maxfiles as libc::rlim_t, rlim.rlim_max); // Set our newly-increased resource limit. - if libc::setrlimit(libc::RLIMIT_NOFILE, &rlim) != 0 { + if unsafe { libc::setrlimit(libc::RLIMIT_NOFILE, &rlim) } != 0 { let err = io::Error::last_os_error(); panic!("raise_fd_limit: error calling setrlimit: {err}"); } diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 7fb484eb07be..c0d267c858dd 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -4,7 +4,7 @@ [package] name = "kani-cov" version = "0.1.0" -edition = "2021" +edition = "2024" license = "MIT OR Apache-2.0" description = "A tool to process coverage information from Kani" diff --git a/tools/scanner/Cargo.toml b/tools/scanner/Cargo.toml index c4d615d3f32d..68d915f5be63 100644 --- a/tools/scanner/Cargo.toml +++ b/tools/scanner/Cargo.toml @@ -6,7 +6,7 @@ name = "scanner" description = "A rustc extension used to scan rust features in a crate" version = "0.0.0" -edition = "2021" +edition = "2024" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs index 08bcc7c04b04..9840c83e1abd 100644 --- a/tools/scanner/src/analysis.rs +++ b/tools/scanner/src/analysis.rs @@ -610,38 +610,37 @@ impl MirVisitor for IteratorVisitor<'_> { if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = kind { let fullname = def.name(); let names = fullname.split("::").collect::>(); - if let [.., s_last, last] = names.as_slice() { - if *s_last == "Iterator" - && [ - "for_each", - "collect", - "advance_by", - "all", - "any", - "partition", - "partition_in_place", - "fold", - "try_fold", - "spec_fold", - "spec_try_fold", - "try_for_each", - "for_each", - "try_reduce", - "reduce", - "find", - "find_map", - "try_find", - "position", - "rposition", - "nth", - "count", - "last", - "find", - ] - .contains(last) - { - self.props.iterators += 1; - } + if let [.., s_last, last] = names.as_slice() + && *s_last == "Iterator" + && [ + "for_each", + "collect", + "advance_by", + "all", + "any", + "partition", + "partition_in_place", + "fold", + "try_fold", + "spec_fold", + "spec_try_fold", + "try_for_each", + "for_each", + "try_reduce", + "reduce", + "find", + "find_map", + "try_find", + "position", + "rposition", + "nth", + "count", + "last", + "find", + ] + .contains(last) + { + self.props.iterators += 1; } } }