Upgrade toolchain to 06/30

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -418,7 +418,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                         name: rustc_span::Symbol::intern(&name.clone()),
                     };
                     let paramenv = TypingEnv::post_analysis(self.tcx, def_id_internal).param_env;
-                    let ty_internal = pc_internal.find_ty_from_env(paramenv);
+                    let ty_internal = pc_internal.find_const_ty_from_env(paramenv);
                     let ty_stable = rustc_internal::stable(ty_internal);
                     let trans_ty = self.translate_ty(ty_stable);
                     let lit_ty = match trans_ty.kind() {
@@ -486,7 +486,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                             index: paramtc.index,
                             name: rustc_span::Symbol::intern(&paramtc.name),
                         };
-                        let ty_internal = pc_internal.find_ty_from_env(paramenv);
+                        let ty_internal = pc_internal.find_const_ty_from_env(paramenv);
                         let ty_stable = rustc_internal::stable(ty_internal);
                         let trans_ty = self.translate_ty(ty_stable);
                         let lit_ty = match trans_ty.kind() {
@@ -568,7 +568,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                             index: paramtc.index,
                             name: rustc_span::Symbol::intern(&paramtc.name),
                         };
-                        let ty_internal = pc_internal.find_ty_from_env(paramenv);
+                        let ty_internal = pc_internal.find_const_ty_from_env(paramenv);
                         let ty_stable = rustc_internal::stable(ty_internal);
                         let trans_ty = self.translate_ty(ty_stable);
                         let lit_ty = match trans_ty.kind() {

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -256,25 +256,23 @@ impl GotocCtx<'_> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
+                // Generate the message to print to the user and property class.
+                // For `msg`s with runtime values, replace them with static messages,
+                // since that's all that CBMC accepts.
                 let (msg, property_class) = match msg {
-                    AssertMessage::BoundsCheck { .. } => {
-                        // For bounds check the following panic message is generated at runtime:
-                        // "index out of bounds: the length is {len} but the index is {index}",
-                        // but CBMC only accepts static messages so we don't add values to the message.
-                        (
-                            "index out of bounds: the length is less than or equal to the given index",
-                            PropertyClass::Assertion,
-                        )
-                    }
-                    AssertMessage::MisalignedPointerDereference { .. } => {
-                        // Misaligned pointer dereference check messages is also a runtime messages.
-                        // Generate a generic one here.
-                        (
-                            "misaligned pointer dereference: address must be a multiple of its type's \
+                    AssertMessage::BoundsCheck { .. } => (
+                        "index out of bounds: the length is less than or equal to the given index",
+                        PropertyClass::Assertion,
+                    ),
+                    AssertMessage::InvalidEnumConstruction { .. } => (
+                        "invalid enum construction: value is not a valid discriminant for this enum",
+                        PropertyClass::SafetyCheck,
+                    ),
+                    AssertMessage::MisalignedPointerDereference { .. } => (
+                        "misaligned pointer dereference: address must be a multiple of its type's \
                     alignment",
-                            PropertyClass::SafetyCheck,
-                        )
-                    }
+                        PropertyClass::SafetyCheck,
+                    ),
                     // For all other assert kind we can get the static message.
                     AssertMessage::NullPointerDereference => {
                         (msg.description().unwrap(), PropertyClass::SafetyCheck)

kani-compiler/src/kani_middle/transform/internal_mir.rs

@@ -514,6 +514,21 @@ impl RustcInternalMir for AssertMessage {
                     index: index.internal_mir(tcx),
                 }
             }
+            AssertMessage::DivisionByZero(operand) => {
+                rustc_middle::mir::AssertMessage::DivisionByZero(operand.internal_mir(tcx))
+            }
+            AssertMessage::InvalidEnumConstruction(source) => {
+                rustc_middle::mir::AssertMessage::InvalidEnumConstruction(source.internal_mir(tcx))
+            }
+            AssertMessage::MisalignedPointerDereference { required, found } => {
+                rustc_middle::mir::AssertMessage::MisalignedPointerDereference {
+                    required: required.internal_mir(tcx),
+                    found: found.internal_mir(tcx),
+                }
+            }
+            AssertMessage::NullPointerDereference => {
+                rustc_middle::mir::AssertMessage::NullPointerDereference
+            }
             AssertMessage::Overflow(bin_op, left_operand, right_operand) => {
                 rustc_middle::mir::AssertMessage::Overflow(
                     internal(tcx, bin_op),
@@ -524,33 +539,21 @@ impl RustcInternalMir for AssertMessage {
             AssertMessage::OverflowNeg(operand) => {
                 rustc_middle::mir::AssertMessage::OverflowNeg(operand.internal_mir(tcx))
             }
-            AssertMessage::DivisionByZero(operand) => {
-                rustc_middle::mir::AssertMessage::DivisionByZero(operand.internal_mir(tcx))
-            }
             AssertMessage::RemainderByZero(operand) => {
                 rustc_middle::mir::AssertMessage::RemainderByZero(operand.internal_mir(tcx))
             }
-            AssertMessage::ResumedAfterReturn(coroutine_kind) => {
-                rustc_middle::mir::AssertMessage::ResumedAfterReturn(
-                    coroutine_kind.internal_mir(tcx),
-                )
+            AssertMessage::ResumedAfterDrop(coroutine_kind) => {
+                rustc_middle::mir::AssertMessage::ResumedAfterDrop(coroutine_kind.internal_mir(tcx))
             }
             AssertMessage::ResumedAfterPanic(coroutine_kind) => {
                 rustc_middle::mir::AssertMessage::ResumedAfterPanic(
                     coroutine_kind.internal_mir(tcx),
                 )
             }
-            AssertMessage::MisalignedPointerDereference { required, found } => {
-                rustc_middle::mir::AssertMessage::MisalignedPointerDereference {
-                    required: required.internal_mir(tcx),
-                    found: found.internal_mir(tcx),
-                }
-            }
-            AssertMessage::NullPointerDereference => {
-                rustc_middle::mir::AssertMessage::NullPointerDereference
-            }
-            AssertMessage::ResumedAfterDrop(coroutine_kind) => {
-                rustc_middle::mir::AssertMessage::ResumedAfterDrop(coroutine_kind.internal_mir(tcx))
+            AssertMessage::ResumedAfterReturn(coroutine_kind) => {
+                rustc_middle::mir::AssertMessage::ResumedAfterReturn(
+                    coroutine_kind.internal_mir(tcx),
+                )
             }
         }
     }

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-06-27"
+channel = "nightly-2025-06-30"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]