diff --git a/.cargo/config.toml b/.cargo/config.toml index f0df939ef506..3ad7072f56cd 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -35,3 +35,12 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -. "-Aclippy::needless-borrow", "-Aclippy::bool-to-int-with-if", ] + +# Doctests are compiled by rustdoc, not through Kani's driver, so they miss the +# `-Znext-solver=coherence` that `base_rustc_flags` passes to every crate Kani compiles. +# `kani::pointer_generator`'s return type uses `generic_const_exprs`, which the +# next-generation trait solver (on by default since nightly-2026-09-22) cannot handle, so the +# doctests that call it need the same setting. +# Tracked for removal in https://github.com/model-checking/kani/issues/4832. +[build] +rustdocflags = ["-Znext-solver=coherence"] diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 42f2ef5e4cb3..44e1c5fd3b61 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -38,9 +38,10 @@ use rustc_public::mir::mono::{Instance, MonoItem}; use rustc_public::rustc_internal; use rustc_public::ty::FnDef; use rustc_public::{CrateDef, DefId}; -use rustc_session::config::{CrateType, OutputFilenames, OutputType}; +use rustc_session::config::{OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_session::{IncrCompSession, Session}; +use rustc_structures::CrateType; use std::any::Any; use std::fs::File; use std::path::Path; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index bc45256d804a..08abcfd9da28 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -297,7 +297,7 @@ pub mod rustc_public_bridge { let filename = rustc_internal::stable(body.span).get_filename(); // Some functions, like `std` ones, may not have coverage info attached // to them because they have been compiled without coverage flags. - if let Some(cov_info) = &body.function_coverage_info { + if let Some(cov_info) = &body.coverage_mir_info { // Iterate over the coverage mappings and match with the coverage term. let mut source_regions: Vec = Vec::new(); for mapping in &cov_info.mappings { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 99da41fdc8ea..f20a25ba275e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -10,7 +10,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type; use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; -use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type}; use rustc_abi::{TagEncoding, Variants}; use rustc_middle::ty::layout::LayoutOf; @@ -681,8 +680,22 @@ impl GotocCtx<'_, '_> { /// and we need to take it's address and build the fat pointer. pub fn codegen_place_ref_stable(&mut self, place: &Place, loc: Location) -> Expr { let place_ty = self.place_ty_stable(place); - let projection = - unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place, loc)); + let projection = match self.codegen_place_stable(place, loc) { + Ok(projection) => projection, + Err(err) => { + // This function yields a *reference* to the place, so the stub that replaces an + // unsupported projection has to have the reference's type (thin or fat), not the + // place's own. `unwrap_or_return_codegen_unimplemented!` would return the latter + // and the caller would then assign a value to a pointer-typed local. + let ref_ty = self.codegen_ty_ref_stable(place_ty); + return self.codegen_unimplemented_expr( + err.operation.as_str(), + ref_ty, + err.loc, + err.bug_url.as_str(), + ); + } + }; if self.use_thin_pointer_stable(place_ty) { // For ZST objects rustc does not necessarily generate any actual objects. let need_not_be_an_object = self.is_zst_object(&projection.goto_expr); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 07593bd5315b..9122667c3c37 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -20,7 +20,7 @@ use cbmc::{InternString, InternedString, btree_string_map}; use num::bigint::BigInt; use rustc_abi::{FieldsShape, TagEncoding, Variants}; use rustc_middle::ty::{TyCtxt, VtblEntry}; -use rustc_public::abi::{Primitive, Scalar, ValueAbi}; +use rustc_public::abi::{Primitive, Scalar, ValueRepr}; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ AggregateKind, BinOp, CastKind, Operand, Place, PointerCoercion, Rvalue, UnOp, @@ -1848,8 +1848,8 @@ impl GotocCtx<'_, '_> { // } // ``` let res_typ = self.codegen_ty_stable(res_ty); - let ValueAbi::Scalar(Scalar::Initialized { value, valid_range }) = - res_ty.layout().unwrap().shape().abi + let ValueRepr::Scalar(Scalar::Initialized { value, valid_range }) = + res_ty.layout().unwrap().shape().value_repr else { unreachable!("Unexpected layout") }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index bf98c7f404a4..fb5cc60e43be 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -938,7 +938,12 @@ impl GotocCtx<'_, '_> { fargs[0] = if self_ty.kind().is_adt() { // Generate a temp variable and assign its inner pointer to the fat_ptr.data. match fn_ptr.typ() { - Type::Pointer { typ: box Type::Code { parameters, .. } } => { + // `box` patterns were removed in nightly-2026-09-22, so match the pointer and + // then look through it. + Type::Pointer { typ } => { + let Type::Code { parameters, .. } = typ.as_ref() else { + unreachable!("Unexpected virtual function type: {:?}", fn_ptr.typ()) + }; let param_typ = parameters.first().unwrap().typ(); let (tmp, decl) = self.decl_temp_variable(param_typ.clone(), None, loc); debug!(?tmp, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index e3396454fd9c..5f5757f778cc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1554,6 +1554,10 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { Float::F32 => self.tcx.types.f32, Float::F64 => self.tcx.types.f64, Float::F128 => self.tcx.types.f128, + // `f16b` (bfloat16) is a library type rather than a primitive, so there is no + // `tcx.types` entry for it, and CBMC has no bfloat16 type either. rustc itself + // declines to map this primitive back to a Rust type (`rustc_abi::layout::ty`). + Float::F16B => unimplemented!("bfloat16 (`f16b`) is not supported by Kani"), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 3fd20e0659bd..9c65098f2343 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -40,10 +40,11 @@ use rustc_public::CrateDef; use rustc_public::mir::mono::{Instance, MonoItem}; use rustc_public::rustc_internal; use rustc_public::ty::FnDef; -use rustc_session::config::{CrateType, OutputFilenames, OutputType}; +use rustc_session::config::{OutputFilenames, OutputType}; use rustc_session::output::out_filename; -use rustc_session::{IncrCompSession, Session}; +use rustc_session::{EarlySession, IncrCompSession, Session}; use rustc_span::{Symbol, sym}; +use rustc_structures::CrateType; use rustc_target::spec::{Arch, Os, PanicStrategy}; use std::any::Any; use std::cmp::min; @@ -293,7 +294,7 @@ impl CodegenBackend for GotocCodegenBackend { "kani-cprover" } - fn target_config(&self, sess: &Session) -> TargetConfig { + fn target_config(&self, sess: &EarlySession) -> TargetConfig { // This code is adapted from the cranelift backend: // https://github.com/rust-lang/rust/blob/a124fb3cb7291d75872934f411d81fe298379ace/compiler/rustc_codegen_cranelift/src/lib.rs#L184 let target_features = if sess.target.arch == Arch::X86_64 && sess.target.os != Os::None { @@ -320,6 +321,8 @@ impl CodegenBackend for GotocCodegenBackend { internal_target_features: UnordSet::from_iter(target_features), has_reliable_f16, has_reliable_f16_math: has_reliable_f16, + // CBMC has no bfloat16 type, so `f16b` is not supported. + has_reliable_f16b: false, has_reliable_f128, has_reliable_f128_math: has_reliable_f128, } 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 e5d1a50a7bda..985028c25b43 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -29,7 +29,6 @@ use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; use rustc_abi::{HasDataLayout, TargetDataLayout}; use rustc_data_structures::fx::FxHashMap; -use rustc_middle::span_bug; use rustc_middle::ty::layout::{ FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasTyCtxt, HasTypingEnv, LayoutError, LayoutOfHelpers, TyAndLayout, @@ -40,6 +39,7 @@ use rustc_public::mir::mono::Instance; use rustc_public::ty::Allocation; use rustc_span::Span; use rustc_span::respan; +use rustc_span::span_bug; use rustc_target::callconv::FnAbi; use std::collections::{BTreeMap, HashMap, HashSet}; use std::fmt::Debug; diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 38b79ddbc223..f4fbdf8cb0e3 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -518,7 +518,7 @@ impl<'tcx> KaniAttributes<'tcx> { ) .with_note(format!("see issue {} for more information", unstable_attr.issue)) .with_help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature)) - .emit() + .emit_err() } /// Is this item a harness? (either `proof` or `proof_for_contract` @@ -1149,7 +1149,7 @@ impl UnstableAttrParseError<'_> { "expected format: #[kani::unstable_feature({}, {}, {})]", r#"feature="""#, r#"issue="""#, r#"reason="""# )) - .emit() + .emit_err() } } diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs index 53ac3ef706e8..fa31ed48f8c3 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs @@ -154,7 +154,11 @@ impl<'tcx> PointsToGraph<'tcx> { HashSet::from([MemLoc::new_stack_allocation(instance, place_without_projections)]); for projection in place.projection { match projection { - ProjectionElem::Deref => { + // A `PhantomDeref` is the borrow checker's symbolic dereference of a + // `Reborrow` type (rust-lang/rust#159103). Treat it as a dereference: it + // reaches an indirect place, so following the pointer keeps the aliasing + // information conservative. + ProjectionElem::Deref | ProjectionElem::PhantomDeref => { node_set = self.successors(&node_set); } ProjectionElem::Field(..) diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 1683f3bad1be..187c5067aa18 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -12,7 +12,6 @@ use tracing::{debug, trace}; use kani_metadata::HarnessMetadata; use rustc_hir::def_id::DefId; use rustc_middle::mir::Const; -use rustc_middle::ty::RegionExt; use rustc_middle::ty::{self, EarlyBinder, TyCtxt, TypeFoldable, TypingEnv}; use rustc_public::mir::ConstOperand; use rustc_public::mir::mono::Instance; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index f413e8f3a1a0..8d21b8dd4d23 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -7,7 +7,7 @@ use std::fmt::Display; use rustc_public::CrateDefType; use rustc_public::{ - abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape}, + abi::{FieldsShape, Scalar, TagEncoding, ValueRepr, VariantsShape}, target::{MachineInfo, MachineSize}, ty::{AdtKind, RigidTy, Ty, TyKind, UintTy, VariantIdx}, }; @@ -184,11 +184,11 @@ fn data_bytes_for_ty( let layout = ty.layout().unwrap().shape(); match layout.fields { - FieldsShape::Primitive => Ok(vec![match layout.abi { - ValueAbi::Scalar(Scalar::Initialized { value, .. }) => { + FieldsShape::Primitive => Ok(vec![match layout.value_repr { + ValueRepr::Scalar(Scalar::Initialized { value, .. }) => { DataBytes { offset: current_offset, size: value.size(machine_info) } } - _ => unreachable!("FieldsShape::Primitive with a different ABI than ValueAbi::Scalar"), + _ => unreachable!("FieldsShape::Primitive with a different ABI than ValueRepr::Scalar"), }]), FieldsShape::Array { stride, count } if count > 0 => { let TyKind::RigidTy(RigidTy::Array(elem_ty, _)) = ty.kind() else { unreachable!() }; @@ -358,12 +358,12 @@ fn data_bytes_for_ty( RigidTy::Str | RigidTy::Slice(_) | RigidTy::Array(_, _) => { unreachable!("Expected array layout for {ty:?}") } - RigidTy::RawPtr(_, _) | RigidTy::Ref(_, _, _) => Ok(match layout.abi { - ValueAbi::Scalar(Scalar::Initialized { value, .. }) => { + RigidTy::RawPtr(_, _) | RigidTy::Ref(_, _, _) => Ok(match layout.value_repr { + ValueRepr::Scalar(Scalar::Initialized { value, .. }) => { // Thin pointer, ABI is a single scalar. vec![DataBytes { offset: current_offset, size: value.size(machine_info) }] } - ValueAbi::ScalarPair { + ValueRepr::ScalarPair { a: Scalar::Initialized { value: value_first, .. }, b: Scalar::Initialized { value: value_second, .. }, .. diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 6c078dd0bf74..0733f0cfe50f 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -22,7 +22,9 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::{Const, TyCtxt}; use rustc_public::CrateDef; use rustc_public::CrateDefType; -use rustc_public::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange}; +use rustc_public::abi::{ + FieldsShape, Scalar, TagEncoding, ValueRepr, VariantsShape, WrappingRange, +}; use rustc_public::mir::mono::Instance; use rustc_public::mir::visit::{Location, PlaceContext, PlaceRef}; use rustc_public::mir::{ @@ -186,7 +188,7 @@ enum ValidityRange { // 3- Ranges intersection is a combination of two new ranges. // 4- Intersection is empty. impl ValidValueReq { - /// Only a type with `ValueAbi::Scalar` and `ValueAbi::ScalarPair` can be directly assigned an + /// Only a type with `ValueRepr::Scalar` and `ValueRepr::ScalarPair` can be directly assigned an /// invalid value directly. /// /// It's not possible to define a `rustc_layout_scalar_valid_range_*` to any other structure. @@ -206,20 +208,20 @@ impl ValidValueReq { }) } else { let shape = ty.layout().unwrap().shape(); - match shape.abi { - ValueAbi::Scalar(Scalar::Initialized { value, valid_range }) - | ValueAbi::ScalarPair { a: Scalar::Initialized { value, valid_range }, .. } => { + match shape.value_repr { + ValueRepr::Scalar(Scalar::Initialized { value, valid_range }) + | ValueRepr::ScalarPair { a: Scalar::Initialized { value, valid_range }, .. } => { Some(ValidValueReq { offset: 0, size: value.size(machine_info), valid_range: ValidityRange::Single(valid_range), }) } - ValueAbi::Scalar(_) - | ValueAbi::ScalarPair { .. } - | ValueAbi::Vector { .. } - | ValueAbi::ScalableVector { .. } - | ValueAbi::Aggregate { .. } => None, + ValueRepr::Scalar(_) + | ValueRepr::ScalarPair { .. } + | ValueRepr::Vector { .. } + | ValueRepr::ScalableVector { .. } + | ValueRepr::Aggregate { .. } => None, } } } @@ -957,7 +959,7 @@ pub fn ty_validity_per_offset( return Err("Unsupported pattern type over `char`".to_string()); } assert!( - matches!(layout.abi, ValueAbi::Scalar(..)), + matches!(layout.value_repr, ValueRepr::Scalar(..)), "expected pattern type to have a scalar ABI: {ty:?}" ); return Ok(ty_req()); diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index f3a91139243d..77fa77176405 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -8,7 +8,6 @@ //! rustc_private feature and a specific version of rustc. #![feature(extern_types)] #![recursion_limit = "256"] -#![feature(box_patterns)] #![feature(rustc_private)] #![feature(iter_intersperse)] #![feature(f128)] @@ -39,6 +38,7 @@ extern crate rustc_public; extern crate rustc_public_bridge; extern crate rustc_session; extern crate rustc_span; +extern crate rustc_structures; extern crate rustc_target; extern crate rustc_trait_selection; // We can't add this directly as a dependency because we need the version to match rustc diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index d6dfcd8c7044..433eabec63c3 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -273,6 +273,14 @@ pub fn base_rustc_flags(lib_config: LibConfig) -> Vec { "crate-attr=feature(register_tool)", "-Z", "crate-attr=register_tool(kanitool)", + // nightly-2026-09-22 turns the next-generation trait solver on by default + // (rust-lang/rust#160619), and that solver cannot handle `generic_const_exprs` + // (rust-lang/rust#160895). rustc reverts to this setting automatically for a crate that + // enables the feature itself, but Kani's library exposes such a signature + // (`kani::pointer_generator`, whose return type computes its buffer length), so every + // crate Kani compiles needs the same setting to be able to call it. Tracked for removal in + // https://github.com/model-checking/kani/issues/4832. + "-Znext-solver=coherence", // Kani injects unstable features (`register_tool` above) into every crate it compiles, // so crates that `forbid(unstable_features)` (e.g. rustls) would fail to build through // no fault of their own. Downgrade that lint to a warning; `--force-warn` overrides diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c5532974f85d..72deac157bf7 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2026-08-21" +channel = "nightly-2026-09-22" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/charon-patch.diff b/scripts/charon-patch.diff index 50dbd8bd5247..83ba6d828463 100644 --- a/scripts/charon-patch.diff +++ b/scripts/charon-patch.diff @@ -150,6 +150,18 @@ index 3cb58353..0d5f88f9 100644 self.vector.indices() } +diff --git a/charon/src/lib.rs b/charon/src/lib.rs +index 62b33782..8eb0728e 100644 +--- a/charon/src/lib.rs ++++ b/charon/src/lib.rs +@@ -14,7 +14,6 @@ + // For rustdoc: prevents overflows + #![recursion_limit = "256"] + #![feature(assert_matches)] +-#![feature(box_patterns)] + #![feature(deref_pure_trait)] + #![feature(if_let_guard)] + #![feature(impl_trait_in_assoc_type)] diff --git a/charon/src/options.rs b/charon/src/options.rs index 5f2960d1..99008474 100644 --- a/charon/src/options.rs @@ -219,6 +231,62 @@ index 5f2960d1..99008474 100644 "`--dest` is deprecated, use `--dest-file` instead", ) } +diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs +index 6730e159..f01fbd07 100644 +--- a/charon/src/pretty/fmt_with_ctx.rs ++++ b/charon/src/pretty/fmt_with_ctx.rs +@@ -1025,14 +1025,17 @@ impl FmtWithCtx for ullbc::Statement { + place.fmt_with_ctx(ctx), + variant_id + ), +- RawStatement::CopyNonOverlapping(box CopyNonOverlapping { src, dst, count }) => write!( +- &mut out, +- "{}copy_nonoverlapping({}, {}, {})", +- tab, +- src.fmt_with_ctx(ctx), +- dst.fmt_with_ctx(ctx), +- count.fmt_with_ctx(ctx), +- ), ++ RawStatement::CopyNonOverlapping(copy) => { ++ let CopyNonOverlapping { src, dst, count } = &**copy; ++ write!( ++ &mut out, ++ "{}copy_nonoverlapping({}, {}, {})", ++ tab, ++ src.fmt_with_ctx(ctx), ++ dst.fmt_with_ctx(ctx), ++ count.fmt_with_ctx(ctx), ++ ) ++ } + RawStatement::StorageLive(var_id) => { + write!( + &mut out, +@@ -1088,14 +1091,17 @@ impl FmtWithCtx for llbc::Statement { + place.fmt_with_ctx(ctx), + variant_id + ), +- RawStatement::CopyNonOverlapping(box CopyNonOverlapping { src, dst, count }) => write!( +- &mut out, +- "{}copy_nonoverlapping({}, {}, {})", +- tab, +- src.fmt_with_ctx(ctx), +- dst.fmt_with_ctx(ctx), +- count.fmt_with_ctx(ctx), +- ), ++ RawStatement::CopyNonOverlapping(copy) => { ++ let CopyNonOverlapping { src, dst, count } = &**copy; ++ write!( ++ &mut out, ++ "{}copy_nonoverlapping({}, {}, {})", ++ tab, ++ src.fmt_with_ctx(ctx), ++ dst.fmt_with_ctx(ctx), ++ count.fmt_with_ctx(ctx), ++ ) ++ } + RawStatement::StorageLive(var_id) => { + write!( + &mut out, diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index cf4dad41..180adf08 100644 --- a/charon/src/transform/check_generics.rs @@ -254,6 +322,28 @@ index c6140aa0..781c109a 100644 let _ = self.compute_extra_params_for_trait(pred.trait_id); self.trait_modifications[pred.trait_id] .as_processed() +diff --git a/charon/src/transform/inline_local_panic_functions.rs b/charon/src/transform/inline_local_panic_functions.rs +index a0327689..31cb929d 100644 +--- a/charon/src/transform/inline_local_panic_functions.rs ++++ b/charon/src/transform/inline_local_panic_functions.rs +@@ -50,15 +50,12 @@ impl UllbcPass for Transform { + if let RawTerminator::Call { + call: + Call { +- func: +- FnOperand::Regular(FnPtr { +- func: box FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)), +- .. +- }), ++ func: FnOperand::Regular(FnPtr { func, .. }), + .. + }, + .. + } = &block.terminator.content ++ && let FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)) = &**func + && panic_fns.contains(fun_id) + { + block.terminator.content = panic_terminator.clone(); diff --git a/charon/src/transform/simplify_constants.rs b/charon/src/transform/simplify_constants.rs index 3664f51b..1c535677 100644 --- a/charon/src/transform/simplify_constants.rs diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected index c978a8c4e5e8..631dcd5b17f5 100644 --- a/tests/coverage/abort/expected +++ b/tests/coverage/abort/expected @@ -14,8 +14,8 @@ 14| 1| }\ 15| 1| if i == 2 {\ 16| | // This should never happen.\ - 17| 0| ```process::exit'''(1);\ + 17| 0| ```process::exit(1)''';\ 18| 1| } \ 19| | }\ - 20| 0| ```assert!'''(false, "This is unreachable");\ + 20| 0| ```assert!(false''', "This is unreachable");\ 21| | }\ diff --git a/tests/coverage/assert/expected b/tests/coverage/assert/expected index 17dbcb42c205..87af35285cd5 100644 --- a/tests/coverage/assert/expected +++ b/tests/coverage/assert/expected @@ -7,12 +7,12 @@ 7| 1| if x > 5 {\ 8| | // fails\ 9| 1| assert!(x < 4);\ - 10| 1| if x < 3 ```{'''\ - 11| 0| ``` // unreachable'''\ - 12| 0| ``` assert!(x == 2);'''\ - 13| 0| ``` ```}''''''\ - 14| 1| } else {\ - 15| 1| // passes\ + 10| 1| if x < 3 {\ + 11| | // unreachable\ + 12| 0| ```assert!(x == 2''');\ + 13| 0| ```}''' \ + 14| | } else {\ + 15| | // passes\ 16| 1| assert!(x <= 5);\ - 17| 1| }\ + 17| | }\ 18| | }\ diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected index 8665bb8bcbeb..943ad8d2c4b6 100644 --- a/tests/coverage/assert_eq/expected +++ b/tests/coverage/assert_eq/expected @@ -5,7 +5,7 @@ 5| 1| fn main() {\ 6| 1| let x: i32 = kani::any();\ 7| 1| let y = if x > 10 { 15 } else { 33 };\ - 8| 1| if y > 50 ```{'''\ - 9| 0| ``` assert_eq!(y, 55);'''\ - 10| 1| ``` }'''\ + 8| 1| if y > 50 {\ + 9| 0| ```assert_eq!(y, 55''');\ + 10| 1| } \ 11| | }\ diff --git a/tests/coverage/assert_ne/expected b/tests/coverage/assert_ne/expected index 73055a14af10..e4c4bb9a34c8 100644 --- a/tests/coverage/assert_ne/expected +++ b/tests/coverage/assert_ne/expected @@ -7,8 +7,8 @@ 7| 1| if x > 0 {\ 8| 1| let y = x / 2;\ 9| 1| // y is strictly less than x\ - 10| 1| if y == x ```{'''\ - 11| 0| ``` assert_ne!(y, 1);'''\ - 12| 1| ``` }'''\ - 13| 1| }\ + 10| 1| if y == x {\ + 11| 0| ```assert_ne!(y, 1''');\ + 12| 1| } \ + 13| 1| } \ 14| | }\ diff --git a/tests/coverage/contradiction/expected b/tests/coverage/contradiction/expected index 7befb09a1f9e..3e2dc7c502cc 100644 --- a/tests/coverage/contradiction/expected +++ b/tests/coverage/contradiction/expected @@ -5,10 +5,10 @@ 5| 1| let x: u8 = kani::any();\ 6| 1| let mut y: u8 = 0;\ 7| 1| if x > 5 {\ - 8| 1| if x < 2 ```{'''\ - 9| 0| ``` y = x;'''\ - 10| 1| ``` }'''\ - 11| 1| } else {\ + 8| 1| if x < 2 {\ + 9| 0| ```y = x''';\ + 10| 1| } \ + 11| | } else {\ 12| 1| assert!(x < 10);\ - 13| 1| }\ + 13| | }\ 14| | }\ diff --git a/tests/coverage/known_issues/assert_uncovered_end/expected b/tests/coverage/known_issues/assert_uncovered_end/expected index 170217d73b31..d7f7f244bb6e 100644 --- a/tests/coverage/known_issues/assert_uncovered_end/expected +++ b/tests/coverage/known_issues/assert_uncovered_end/expected @@ -10,5 +10,5 @@ 10| 1| let x: u32 = kani::any_where(|val| *val == 5);\ 11| 1| if x > 3 {\ 12| 1| assert!(x > 4);\ - 13| 1| ```}'''\ + 13| 0| ```}'''\ 14| | }\ diff --git a/tests/coverage/known_issues/variant/expected b/tests/coverage/known_issues/variant/expected index 715a5440e0ae..9243924f7b92 100644 --- a/tests/coverage/known_issues/variant/expected +++ b/tests/coverage/known_issues/variant/expected @@ -1,30 +1,30 @@ 1| | // Copyright Kani Contributors\ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ - 3| |\ + 3| | \ 4| | //! Checks coverage results in an example with a `match` statement matching on\ 5| | //! all enum variants. Currently, it does not yield the expected results because\ 6| | //! it reports the `dir` in the match statement as `UNCOVERED`:\ 7| | //! \ - 8| |\ + 8| | \ 9| | enum Direction {\ 10| | Up,\ 11| | Down,\ 12| | Left,\ 13| | Right,\ 14| | }\ - 15| |\ + 15| | \ 16| 1| fn print_direction(dir: Direction) {\ - 17| | // For some reason, `dir`'s span is reported as `UNCOVERED` too\ - 18| 0| match ```dir''' {\ - 19| 0| Direction::Up => ```println!'''("Going up!"),\ - 20| 0| Direction::Down => ```println!'''("Going down!"),\ + 17| 1| // For some reason, `dir`'s span is reported as `UNCOVERED` too\ + 18| 1| match dir {\ + 19| 0| Direction::Up => ```println!("Going up!"'''),\ + 20| 0| Direction::Down => ```println!("Going down!"'''),\ 21| 1| Direction::Left => println!("Going left!"),\ - 22| 0| Direction::Right if 1 == ```1 => println!'''("Going right!"),\ + 22| 0| Direction::Right if ```1 == 1''' => ```println!("Going right!"'''),\ 23| | // This part is unreachable since we cover all variants in the match.\ - 24| 0| _ => ```println!'''("Not going anywhere!"),\ + 24| 0| _ => ```println!("Not going anywhere!"'''),\ 25| | }\ 26| | }\ - 27| |\ + 27| | \ 28| | #[kani::proof]\ 29| 1| fn main() {\ 30| 1| let direction = Direction::Left;\ diff --git a/tests/kani/Intrinsics/Math/Trigonometry/cosf32.rs b/tests/kani/Intrinsics/Math/Trigonometry/cosf32.rs index 7cd13343bd61..6fcea0153319 100644 --- a/tests/kani/Intrinsics/Math/Trigonometry/cosf32.rs +++ b/tests/kani/Intrinsics/Math/Trigonometry/cosf32.rs @@ -1,12 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `cosf32` returns the expected results. +// Check that `f32::cos` returns the expected results. +// (nightly-2026-09-22 removed the `cosf32` intrinsic that used to back it.) // -// The CBMC model for `cosf32` is an overapproximation that returns: +// The CBMC model for `cos` is an overapproximation that returns: // * 1.0 if the argument is 0.0 // * A symbolic value between -1.0 and 1.0 otherwise -#![feature(core_intrinsics)] fn fp_equals(value: f32, expected: f32) -> bool { let abs_diff = (value - expected).abs(); @@ -17,14 +17,14 @@ fn fp_equals(value: f32, expected: f32) -> bool { fn cosine_range() { let x: f32 = kani::any(); kani::assume(x.is_finite()); - let cosine = unsafe { std::intrinsics::cosf32(x) }; + let cosine = x.cos(); assert!(cosine < 1.0 || fp_equals(cosine, 1.0)); assert!(cosine > -1.0 || fp_equals(cosine, -1.0)); } #[kani::proof] fn cosine_const() { - let x = 0.0; - let cosine = unsafe { std::intrinsics::cosf32(x) }; + let x: f32 = 0.0; + let cosine = x.cos(); assert!(fp_equals(cosine, 1.0)); } diff --git a/tests/kani/Intrinsics/Math/Trigonometry/cosf64.rs b/tests/kani/Intrinsics/Math/Trigonometry/cosf64.rs index 2f18013da6f7..6f75da4d1ea8 100644 --- a/tests/kani/Intrinsics/Math/Trigonometry/cosf64.rs +++ b/tests/kani/Intrinsics/Math/Trigonometry/cosf64.rs @@ -1,12 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `cosf64` returns the expected results. +// Check that `f64::cos` returns the expected results. +// (nightly-2026-09-22 removed the `cosf64` intrinsic that used to back it.) // -// The CBMC model for `cosf64` is an overapproximation that returns: +// The CBMC model for `cos` is an overapproximation that returns: // * 1.0 if the argument is 0.0 // * A symbolic value between -1.0 and 1.0 otherwise -#![feature(core_intrinsics)] fn fp_equals(value: f64, expected: f64) -> bool { let abs_diff = (value - expected).abs(); @@ -17,14 +17,14 @@ fn fp_equals(value: f64, expected: f64) -> bool { fn cosine_range() { let x: f64 = kani::any(); kani::assume(x.is_finite()); - let cosine = unsafe { std::intrinsics::cosf64(x) }; + let cosine = x.cos(); assert!(cosine < 1.0 || fp_equals(cosine, 1.0)); assert!(cosine > -1.0 || fp_equals(cosine, -1.0)); } #[kani::proof] fn cosine_const() { - let x = 0.0; - let cosine = unsafe { std::intrinsics::cosf64(x) }; + let x: f64 = 0.0; + let cosine = x.cos(); assert!(fp_equals(cosine, 1.0)); } diff --git a/tests/kani/Intrinsics/Math/Trigonometry/sinf32.rs b/tests/kani/Intrinsics/Math/Trigonometry/sinf32.rs index 85c18d260d31..24e5bb1d7638 100644 --- a/tests/kani/Intrinsics/Math/Trigonometry/sinf32.rs +++ b/tests/kani/Intrinsics/Math/Trigonometry/sinf32.rs @@ -1,13 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `sinf32` returns the expected results. +// Check that `f32::sin` returns the expected results. +// (nightly-2026-09-22 removed the `sinf32` intrinsic that used to back it.) // -// The CBMC model for `sinf32` is an overapproximation that returns: +// The CBMC model for `sin` is an overapproximation that returns: // * 0.0 if the argument is 0.0 // * A symbolic value between -1.0 and 1.0 otherwise -#![feature(core_intrinsics)] fn fp_equals(value: f32, expected: f32) -> bool { let abs_diff = (value - expected).abs(); @@ -18,14 +18,14 @@ fn fp_equals(value: f32, expected: f32) -> bool { fn sine_range() { let x: f32 = kani::any(); kani::assume(x.is_finite()); - let sine = unsafe { std::intrinsics::sinf32(x) }; + let sine = x.sin(); assert!(sine < 1.0 || fp_equals(sine, 1.0)); assert!(sine > -1.0 || fp_equals(sine, -1.0)); } #[kani::proof] fn sine_const() { - let x = 0.0; - let sine = unsafe { std::intrinsics::sinf32(x) }; + let x: f32 = 0.0; + let sine = x.sin(); assert!(fp_equals(sine, 0.0)); } diff --git a/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs b/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs index 3ab111ce8e53..99298dea24c9 100644 --- a/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs +++ b/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs @@ -1,12 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `sinf64` returns the expected results. +// Check that `f64::sin` returns the expected results. +// (nightly-2026-09-22 removed the `sinf64` intrinsic that used to back it.) // -// The CBMC model for `sinf64` is an overapproximation that returns: +// The CBMC model for `sin` is an overapproximation that returns: // * 0.0 if the argument is 0.0 // * A symbolic value between -1.0 and 1.0 otherwise -#![feature(core_intrinsics)] fn fp_equals(value: f64, expected: f64) -> bool { let abs_diff = (value - expected).abs(); @@ -17,14 +17,14 @@ fn fp_equals(value: f64, expected: f64) -> bool { fn sine_range() { let x: f64 = kani::any(); kani::assume(x.is_finite()); - let sine = unsafe { std::intrinsics::sinf64(x) }; + let sine = x.sin(); assert!(sine < 1.0 || fp_equals(sine, 1.0)); assert!(sine > -1.0 || fp_equals(sine, -1.0)); } #[kani::proof] fn sine_const() { - let x = 0.0; - let sine = unsafe { std::intrinsics::sinf64(x) }; + let x: f64 = 0.0; + let sine = x.sin(); assert!(fp_equals(sine, 0.0)); } diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected b/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected index 038d2c9ef14b..607450891ec5 100644 --- a/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected +++ b/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected @@ -1,27 +1,26 @@ -Kani generated automatic harnesses for 9 function(s): -+----------------------------+----------------------------------------------------------------------+ -| Crate | Selected Function | -+===================================================================================================+ -| autoderive_arbitrary_enums | ::assert_fields_are_eq | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | ::eq | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | should_derive::alignment_fail | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | should_derive::alignment_pass | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | should_derive::foo | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | should_derive::generic_recursively_eligible | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | should_derive::multiple_generics_test | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | should_derive::partially_used_generics_test | -|----------------------------+----------------------------------------------------------------------| -| autoderive_arbitrary_enums | should_derive::recursively_eligible | -+----------------------------+----------------------------------------------------------------------+ +Kani generated automatic harnesses for 8 function(s): ++----------------------------+-----------------------------------------------------------+ +| Crate | Selected Function | ++========================================================================================+ +| autoderive_arbitrary_enums | ::eq | +|----------------------------+-----------------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::alignment_fail | +|----------------------------+-----------------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::alignment_pass | +|----------------------------+-----------------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::foo | +|----------------------------+-----------------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::generic_recursively_eligible | +|----------------------------+-----------------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::multiple_generics_test | +|----------------------------+-----------------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::partially_used_generics_test | +|----------------------------+-----------------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::recursively_eligible | ++----------------------------+-----------------------------------------------------------+ Kani did not generate automatic harnesses for 5 function(s). +If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 +----------------------------+----------------------------------------------+----------------------------------------------------------------------------------------------------------------+ | Crate | Skipped Function | Reason for Skipping | +============================================================================================================================================================================================+ @@ -65,24 +64,25 @@ multiple_generics_test.assertion\ - Description: "assertion failed: n % 2 > 0" Autoharness Summary: -+----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------+ -| Crate | Selected Function | Kind of Automatic Harness | Verification Result | -+=======================================================================================================================================================+ -| autoderive_arbitrary_enums | ::assert_fields_are_eq | #[kani::proof] | Success | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | ::eq | #[kani::proof] | Success | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | should_derive::alignment_pass | #[kani::proof_for_contract] | Success | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | should_derive::generic_recursively_eligible | #[kani::proof] | Success | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | should_derive::partially_used_generics_test | #[kani::proof] | Success | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | should_derive::recursively_eligible | #[kani::proof] | Success | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | should_derive::alignment_fail | #[kani::proof] | Failure | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | should_derive::foo | #[kani::proof] | Failure | -|----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_enums | should_derive::multiple_generics_test | #[kani::proof] | Failure | -+----------------------------+----------------------------------------------------------------------+-----------------------------+---------------------+ ++----------------------------+-----------------------------------------------------------+-----------------------------+---------------------+ +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | ++============================================================================================================================================+ +| autoderive_arbitrary_enums | ::eq | #[kani::proof] | Success | +|----------------------------+-----------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::alignment_pass | #[kani::proof_for_contract] | Success | +|----------------------------+-----------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::generic_recursively_eligible | #[kani::proof] | Success | +|----------------------------+-----------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::partially_used_generics_test | #[kani::proof] | Success | +|----------------------------+-----------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::recursively_eligible | #[kani::proof] | Success | +|----------------------------+-----------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::alignment_fail | #[kani::proof] | Failure | +|----------------------------+-----------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::foo | #[kani::proof] | Failure | +|----------------------------+-----------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::multiple_generics_test | #[kani::proof] | Failure | ++----------------------------+-----------------------------------------------------------+-----------------------------+---------------------+ +Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. +If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). +Complete - 5 successfully verified functions, 3 failures, 8 total. diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected index 557db797d23f..9e3fb06f6ea2 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected +++ b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected @@ -1,4 +1,4 @@ -Kani generated automatic harnesses for 17 function(s): +Kani generated automatic harnesses for 16 function(s): +------------------------------+------------------------------------------------------------------------+ | Crate | Selected Function | +=======================================================================================================+ @@ -6,8 +6,6 @@ Kani generated automatic harnesses for 17 function(s): |------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | ::eq | |------------------------------+------------------------------------------------------------------------| -| autoderive_arbitrary_structs | ::assert_fields_are_eq | -|------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | ::eq | |------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | should_derive::alignment_fail | @@ -120,8 +118,6 @@ Autoharness Summary: |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | ::eq | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_structs | ::assert_fields_are_eq | #[kani::proof] | Success | -|------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | ::eq | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | should_derive::alignment_pass | #[kani::proof_for_contract] | Success | diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 884b078f1e77..d965073b816e 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -266,7 +266,8 @@ pub fn run_tests(config: Config) { // `run_tests_console` now takes a tagged list. compiletest collects tests by walking // directories, so the order is not by name and must be reported as `Unsorted`: the // harness binary-searches a list tagged `Sorted`. - let tests = test::TestList::new(tests, test::TestListOrder::Unsorted); + let test_refs: Vec<&test::TestDescAndFn> = tests.iter().collect(); + let tests = test::TestList::new(&test_refs, test::TestListOrder::Unsorted); let res = test::run_tests_console(&opts, tests); match res { Ok(true) => {} @@ -596,8 +597,8 @@ fn make_test_name(config: &Config, testpaths: &TestPaths) -> test::TestName { fn make_test_closure(config: &Config, testpaths: &TestPaths) -> test::TestFn { let config = config.clone(); let testpaths = testpaths.clone(); - test::DynTestFn(Box::new(move || { - runtest::run(config, &testpaths); + test::DynTestFn(std::sync::Arc::new(move || { + runtest::run(config.clone(), &testpaths); Ok(()) })) }