Upgrade Rust toolchain to 2025-10-12

cprover_bindings/src/goto_program/expr.rs

@@ -1687,11 +1687,6 @@ impl Expr {
         Stmt::assign(self, rhs, loc)
     }
 
-    /// Shorthand to build a `Deinit(self)` statement. See `StmtBody::Deinit`
-    pub fn deinit(self, loc: Location) -> Stmt {
-        Stmt::deinit(self, loc)
-    }
-
     /// `if (self) { t } else { e }` or `if (self) { t }`
     pub fn if_then_else(self, t: Stmt, e: Option<Stmt>, loc: Location) -> Stmt {
         Stmt::if_then_else(self, t, e, loc)

cprover_bindings/src/goto_program/stmt.rs

@@ -64,8 +64,6 @@ pub enum StmtBody {
         lhs: Expr, // SymbolExpr
         value: Option<Expr>,
     },
-    /// Marks the target place as uninitialized.
-    Deinit(Expr),
     /// `e;`
     Expression(Expr),
     // `for (init; cond; update) {body}`
@@ -252,11 +250,6 @@ impl Stmt {
         stmt!(Decl { lhs, value }, loc)
     }
 
-    /// `Deinit(place)`, see `StmtBody::Deinit`.
-    pub fn deinit(place: Expr, loc: Location) -> Self {
-        stmt!(Deinit(place), loc)
-    }
-
     /// `e;`
     pub fn code_expression(e: Expr, loc: Location) -> Self {
         stmt!(Expression(e), loc)

cprover_bindings/src/irep/to_irep.rs

@@ -541,13 +541,6 @@ impl ToIrep for StmtBody {
                     code_irep(IrepId::Decl, vec![lhs.to_irep(mm)])
                 }
             }
-            StmtBody::Deinit(place) => {
-                // CBMC doesn't yet have a notion of poison (https://github.com/diffblue/cbmc/issues/7014)
-                // So we translate identically to `nondet` here, but add a comment noting we wish it were poison
-                // potentially for other backends to pick up and treat specially.
-                code_irep(IrepId::Assign, vec![place.to_irep(mm), place.typ().nondet().to_irep(mm)])
-                    .with_comment("deinit")
-            }
             StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
             StmtBody::For { init, cond, update, body } => code_irep(
                 IrepId::For,

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

@@ -129,7 +129,6 @@ impl GotocCtx<'_, '_> {
                     .assign(self.codegen_rvalue_stable(rhs, location), location)
                 }
             }
-            StatementKind::Deinit(place) => self.codegen_deinit(place, location),
             StatementKind::SetDiscriminant { place, variant_index } => {
                 let dest_ty = self.place_ty_stable(place);
                 let dest_expr = unwrap_or_return_codegen_unimplemented_stmt!(
@@ -444,27 +443,6 @@ impl GotocCtx<'_, '_> {
         }
     }
 
-    /// From rustc doc: "This writes `uninit` bytes to the entire place."
-    /// Our model of GotoC has a similar statement, which is later lowered
-    /// to assigning a Nondet in CBMC, with a comment specifying that it
-    /// corresponds to a Deinit.
-    fn codegen_deinit(&mut self, place: &Place, loc: Location) -> Stmt {
-        let dst_mir_ty = self.place_ty_stable(place);
-        let dst_type = self.codegen_ty_stable(dst_mir_ty);
-        let layout = self.layout_of_stable(dst_mir_ty);
-        if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
-            // We ignore assignment for all zero size types
-            Stmt::skip(loc)
-        } else {
-            unwrap_or_return_codegen_unimplemented_stmt!(
-                self,
-                self.codegen_place_stable(place, loc)
-            )
-            .goto_expr
-            .deinit(loc)
-        }
-    }
-
     /// A special case handler to codegen `return ();`
     fn codegen_ret_unit(&mut self, loc: Location) -> Stmt {
         let is_file_local = false;

kani-compiler/src/kani_middle/analysis.rs

@@ -123,7 +123,6 @@ impl From<&Statement> for Key {
     fn from(value: &Statement) -> Self {
         match value.kind {
             StatementKind::Assign(..) => Key("Assign"),
-            StatementKind::Deinit(_) => Key("Deinit"),
             StatementKind::Intrinsic(_) => Key("Intrinsic"),
             StatementKind::SetDiscriminant { .. } => Key("SetDiscriminant"),
             // For now, we don't care about the ones below.

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

@@ -171,7 +171,6 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
             }
             StatementKind::FakeRead(..)
             | StatementKind::SetDiscriminant { .. }
-            | StatementKind::Deinit(..)
             | StatementKind::StorageLive(..)
             | StatementKind::StorageDead(..)
             | StatementKind::Retag(..)

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

@@ -569,7 +569,6 @@ pub trait MutMirVisitor {
             },
             StatementKind::FakeRead(_, _)
             | StatementKind::SetDiscriminant { .. }
-            | StatementKind::Deinit(_)
             | StatementKind::StorageLive(_)
             | StatementKind::StorageDead(_)
             | StatementKind::Retag(_, _)

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs

@@ -220,14 +220,6 @@ impl MirVisitor for CheckUninitVisitor {
                     }
                 }
             }
-            StatementKind::Deinit(place) => {
-                self.super_statement(stmt, location);
-                self.push_target(MemoryInitOp::Set {
-                    operand: Operand::Copy(place.clone()),
-                    value: false,
-                    position: InsertPosition::After,
-                });
-            }
             StatementKind::FakeRead(_, _)
             | StatementKind::SetDiscriminant { .. }
             | StatementKind::StorageLive(_)

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

@@ -411,7 +411,6 @@ impl MirVisitor for CheckValueVisitor<'_, '_> {
                 }
                 StatementKind::FakeRead(_, _)
                 | StatementKind::SetDiscriminant { .. }
-                | StatementKind::Deinit(_)
                 | StatementKind::StorageLive(_)
                 | StatementKind::StorageDead(_)
                 | StatementKind::Retag(_, _)

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

@@ -381,9 +381,6 @@ impl RustcInternalMir for StatementKind {
                     variant_index: internal(tcx, variant_index),
                 }
             }
-            StatementKind::Deinit(place) => {
-                rustc_middle::mir::StatementKind::Deinit(internal(tcx, place).into())
-            }
             StatementKind::StorageLive(local) => rustc_middle::mir::StatementKind::StorageLive(
                 rustc_middle::mir::Local::from_usize(*local),
             ),

rust-toolchain.toml

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