diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 60f2e0f6a101..147bc17eda6a 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -1437,7 +1437,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }; CharonTy::new(CharonTyKind::Arrow(rb)) } - RigidTy::Dynamic(_, _, _) => { + RigidTy::Dynamic(_, _) => { CharonTy::new(CharonTyKind::DynTrait(CharonExistentialPredicate)) } _ => todo!("Not yet implemented RigidTy: {:?}", rigid_ty), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 91f99042ccfa..e9b1fe86f54a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1145,7 +1145,7 @@ impl GotocCtx<'_, '_> { match dst_subt.kind() { TyKind::RigidTy(RigidTy::Slice(_)) | TyKind::RigidTy(RigidTy::Str) - | TyKind::RigidTy(RigidTy::Dynamic(_, _, _)) => { + | TyKind::RigidTy(RigidTy::Dynamic(_, _)) => { //TODO: this does the wrong thing on Strings/fixme_boxed_str.rs // if we cast to slice or string, then we know the source is also a slice or string, // so there shouldn't be anything to do diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index cd94168d0244..22c7fe469020 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -25,7 +25,7 @@ use rustc_public::mir::Body; use rustc_public::mir::mono::Instance as InstanceStable; use rustc_public::rustc_internal; use rustc_public::ty::{ - Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy, + Binder, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy, Ty as StableTy, }; use rustc_span::def_id::DefId; @@ -301,8 +301,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { predictates.extend( projections.into_iter().map(|proj| proj.map_bound(ExistentialPredicate::Projection)), ); - let rigid = - RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }, DynKind::Dyn); + let rigid = RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }); rustc_public::ty::Ty::from_rigid_kind(rigid) } @@ -419,7 +418,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { /// We follow the order from the `TyCtxt::COMMON_VTABLE_ENTRIES`. fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec { let mut vtable_base = common_vtable_fields(self.trait_vtable_drop_type(t)); - if let ty::Dynamic(binder, _, _) = t.kind() { + if let ty::Dynamic(binder, _) = t.kind() { // The virtual methods on the trait ref. Some auto traits have no methods. if let Some(principal) = binder.principal() { let poly = principal.with_self_ty(self.tcx, t); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index af48b0428666..79270d326f18 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -418,7 +418,7 @@ impl MirVisitor for CheckUninitVisitor { .rigid() .expect("should be working with monomorphized code") { - RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { + RigidTy::Adt(..) | RigidTy::Dynamic(_, _) => { self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, 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 ee219114f714..e0b06472a7f1 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 @@ -398,7 +398,7 @@ fn data_bytes_for_ty( | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) - | RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)), + | RigidTy::Dynamic(_, _) => Err(LayoutComputationError::UnsupportedType(ty)), } } FieldsShape::Union(_) => Err(LayoutComputationError::UnionAsField(ty)), diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index d992f2749df4..f4652dcb27cd 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -1061,7 +1061,7 @@ pub fn ty_validity_per_offset( | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) - | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")), + | RigidTy::Dynamic(_, _) => Err(format!("Unsupported {ty:?}")), } } FieldsShape::Union(_) | FieldsShape::Array { .. } => { diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 27f2f3fed725..3eeede9f68e4 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -145,27 +145,24 @@ impl KaniSession { .await) }; - let verification_results = if res.is_err() { + if let Ok(output) = res { + // The timeout wasn't reached + Ok(VerificationResult::from(output?, harness.attributes.should_panic, start_time)) + } else { // An error occurs if the timeout was reached // Kill the process cbmc_process.kill().await?; - VerificationResult { + Ok(VerificationResult { status: VerificationStatus::Failure, failed_properties: FailedProperties::None, results: Err(ExitStatus::Timeout), runtime: start_time.elapsed(), generated_concrete_test: false, coverage_results: None, - } - } else { - // The timeout wasn't reached - let output = res.unwrap()?; - VerificationResult::from(output, harness.attributes.should_panic, start_time) - }; - - Ok(verification_results) + }) + } } /// "Internal," but also used by call_cbmc_viewer diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 5377a788846f..079ec6a9fb30 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-09-18" +channel = "nightly-2025-09-19" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]