diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 31f8da6f32a4..d7fcd4e2f964 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -791,15 +791,6 @@ impl GotocCtx<'_> { e, t, ) => self.codegen_misc_cast(e, *t), - Rvalue::Cast(CastKind::DynStar, _, _) => { - let ty = self.codegen_ty_stable(res_ty); - self.codegen_unimplemented_expr( - "CastKind::DynStar", - ty, - loc, - "https://github.com/model-checking/kani/issues/1784", - ) - } Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => { self.codegen_pointer_cast(k, e, *t, loc) } diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 26c337446ad6..988e01857afb 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -17,7 +17,6 @@ use crate::args::ExtraChecks; use crate::kani_middle::transform::body::{ CheckType, InsertPosition, MutableBody, SourceInstruction, }; -use crate::kani_middle::transform::check_values::SourceOp::UnsupportedCheck; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::{Const, TyCtxt}; @@ -640,12 +639,6 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { }) } } - // `DynStar` is not currently supported in Kani. - // TODO: https://github.com/model-checking/kani/issues/1784 - CastKind::DynStar => self.push_target(UnsupportedCheck { - check: "Dyn*".to_string(), - ty: (rvalue.ty(self.locals).unwrap()), - }), CastKind::PointerExposeAddress | CastKind::PointerWithExposedProvenance | CastKind::PointerCoercion(_) diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 1657f0867f65..ad9d0906f313 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -139,10 +139,6 @@ impl RustcInternalMir for CastKind { CoercionSource::Implicit, ) } - CastKind::DynStar => rustc_middle::mir::CastKind::PointerCoercion( - rustc_ty::adjustment::PointerCoercion::DynStar, - CoercionSource::Implicit, - ), CastKind::IntToInt => rustc_middle::mir::CastKind::IntToInt, CastKind::FloatToInt => rustc_middle::mir::CastKind::FloatToInt, CastKind::FloatToFloat => rustc_middle::mir::CastKind::FloatToFloat, diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 3452484c5054..875e3310ea93 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -12,7 +12,6 @@ #![feature(rustc_private)] #![feature(more_qualified_paths)] #![feature(iter_intersperse)] -#![feature(let_chains)] #![feature(f128)] #![feature(f16)] #![feature(non_exhaustive_omitted_patterns_lint)] diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 972cbd5dfbd3..be86d65dc0f3 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -#![feature(let_chains)] use std::ffi::OsString; use std::process::ExitCode; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 42a4e2ec1383..9e32c0a59e99 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-07-02" +channel = "nightly-2025-07-04" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]