Bump rustc to remove ShallowInitBox

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.197"
+let supported_charon_version = "0.1.198"

charon-ml/src/Print.ml

@@ -936,8 +936,6 @@ and rvalue_to_string (env : fmt_env) (rv : rvalue) : string =
       "[" ^ operand_to_string env v ^ ";"
       ^ constant_expr_to_string env len
       ^ "]"
-  | ShallowInitBox (op, _) ->
-      "shallow-init-box(" ^ operand_to_string env op ^ ")"
   | Aggregate (akind, ops) -> aggregate_to_string env akind ops
 
 let item_id_to_string (id : item_id) : string =

charon-ml/src/generated/Generated_Expressions.ml

@@ -310,11 +310,6 @@ and rvalue =
       (** [Repeat(x, n)] creates an array where [x] is copied [n] times.
 
           We translate this to a function call for LLBC. *)
-  | ShallowInitBox of operand * ty
-      (** Transmutes a [*mut u8] (obtained from [malloc]) into
-          shallow-initialized [Box<T>]. This only appears as part of lowering
-          [Box::new()] in some cases. We reconstruct the original [Box::new()]
-          call, but sometimes may fail to do so, leaking the expression. *)
 
 (** Unary operation *)
 and unop =

charon-ml/src/generated/Generated_OfJson.ml

@@ -1137,10 +1137,6 @@ and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
         let* x_1 = ty_of_json ctx x_1 in
         let* x_2 = box_of_json constant_expr_of_json ctx x_2 in
         Ok (Repeat (x_0, x_1, x_2))
-    | `Assoc [ ("ShallowInitBox", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = operand_of_json ctx x_0 in
-        let* x_1 = ty_of_json ctx x_1 in
-        Ok (ShallowInitBox (x_0, x_1))
     | _ -> Error "")
 
 and scalar_value_of_json (ctx : of_json_ctx) (js : json) :

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -1048,10 +1048,6 @@ and rvalue_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
          let* x_1 = ty_of_postcard ctx st in
          let* x_2 = box_of_postcard constant_expr_of_postcard ctx st in
          Ok (Repeat (x_0, x_1, x_2))
-     | 10 ->
-         let* x_0 = operand_of_postcard ctx st in
-         let* x_1 = ty_of_postcard ctx st in
-         Ok (ShallowInitBox (x_0, x_1))
      | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag))
 
 and scalar_value_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :

charon/Cargo.toml

@@ -24,7 +24,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 
 [package]
 name = "charon"
-version = "0.1.197"
+version = "0.1.198"
 authors.workspace = true
 edition.workspace = true
 license.workspace = true

charon/rust-toolchain

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2026-02-07"
+channel = "nightly-2026-02-22"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-src", "miri" ]
 targets = [ "x86_64-unknown-linux-gnu", "x86_64-apple-darwin", "x86_64-pc-windows-msvc", "aarch64-apple-darwin", "i686-unknown-linux-gnu", "powerpc64-unknown-linux-gnu", "riscv64gc-unknown-none-elf" ]

charon/src/ast/builtins.rs

@@ -12,6 +12,15 @@ use crate::types::*;
 // We treat this one specially in the `inline_local_panic_functions` pass. See there for details.
 pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit"];
 
+pub static BOX_ASSUME_INIT_INTO_VEC_UNSAFE: &str = "box_assume_init_into_vec_unsafe";
+
+pub static BOX_WRITE: &str = "alloc::boxed::Box::write";
+
+// The translated Charon name contains an inherent impl path element where the Rust path contains
+// `Box`. `NamePattern` does not yet inspect inherent impl receiver types, so passes that match the
+// translated name need this wildcarded pattern.
+pub static BOX_WRITE_PATTERN: &str = "alloc::boxed::_::write";
+
 impl BuiltinTy {
     pub fn get_name(self) -> Name {
         let name: &[_] = match self {

charon/src/ast/expressions.rs

@@ -753,10 +753,6 @@ pub enum Rvalue {
     ///
     /// We translate this to a function call for LLBC.
     Repeat(Operand, Ty, Box<ConstantExpr>),
-    /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. This
-    /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original
-    /// `Box::new()` call, but sometimes may fail to do so, leaking the expression.
-    ShallowInitBox(Operand, Ty),
 }
 
 /// An aggregated ADT.

charon/src/ast/hash_cons.rs

@@ -77,7 +77,6 @@ mod intern_table {
         U: indexmap::Equivalent<Arc<T>>,
     {
         // Fast read-only check.
-        #[expect(irrefutable_let_patterns)] // https://github.com/rust-lang/rust/issues/139369
         let arc = if let read_guard = INTERNED.read().unwrap()
             && let Some(map) = read_guard.get::<T>()
             && let Some((arc, _id)) = map.get_key_value(&inner)

charon/src/ast/types_utils.rs

@@ -758,6 +758,10 @@ impl Ty {
         }
     }
 
+    pub fn as_adt_id(&self) -> Option<TypeDeclId> {
+        self.kind().as_adt().and_then(|a| a.id.as_adt().cloned())
+    }
+
     pub fn get_ptr_metadata(&self, translated: &TranslatedCrate) -> PtrMetadata {
         let ty_decls = &translated.type_decls;
         match self.kind() {

charon/src/ast/ullbc_ast_utils.rs

@@ -6,6 +6,33 @@ use crate::meta::Span;
 use crate::ullbc_ast::*;
 use std::collections::HashMap;
 use std::mem;
+use std::ops::{Index, IndexMut};
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct StmtLoc {
+    pub block: BlockId,
+    pub statement: usize,
+}
+
+impl StmtLoc {
+    pub fn new(block: BlockId, statement: usize) -> Self {
+        StmtLoc { block, statement }
+    }
+
+    pub fn block_start(block: BlockId) -> Self {
+        StmtLoc {
+            block,
+            statement: 0,
+        }
+    }
+
+    pub fn after(self) -> Self {
+        StmtLoc {
+            block: self.block,
+            statement: self.statement + 1,
+        }
+    }
+}
 
 impl SwitchTargets {
     pub fn targets(&self) -> SmallVec<[BlockId; 2]> {
@@ -118,6 +145,23 @@ impl Terminator {
             }
         }
     }
+
+    pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> {
+        match &self.kind {
+            TerminatorKind::Goto { target } => {
+                smallvec![*target]
+            }
+            TerminatorKind::Switch { targets, .. } => targets.targets(),
+            TerminatorKind::Call { target, .. }
+            | TerminatorKind::Drop { target, .. }
+            | TerminatorKind::Assert { target, .. } => {
+                smallvec![*target]
+            }
+            TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => {
+                smallvec![]
+            }
+        }
+    }
 }
 
 impl BlockData {
@@ -165,22 +209,8 @@ impl BlockData {
     pub fn targets(&self) -> SmallVec<[BlockId; 2]> {
         self.terminator.targets()
     }
-
     pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> {
-        match &self.terminator.kind {
-            TerminatorKind::Goto { target } => {
-                smallvec![*target]
-            }
-            TerminatorKind::Switch { targets, .. } => targets.targets(),
-            TerminatorKind::Call { target, .. }
-            | TerminatorKind::Drop { target, .. }
-            | TerminatorKind::Assert { target, .. } => {
-                smallvec![*target]
-            }
-            TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => {
-                smallvec![]
-            }
-        }
+        self.terminator.targets_ignoring_unwind()
     }
 
     /// Apply a transformer to all the statements.
@@ -304,6 +334,19 @@ impl ExprBody {
     }
 }
 
+impl Index<StmtLoc> for ExprBody {
+    type Output = Statement;
+    fn index(&self, loc: StmtLoc) -> &Self::Output {
+        &self.body[loc.block].statements[loc.statement]
+    }
+}
+
+impl IndexMut<StmtLoc> for ExprBody {
+    fn index_mut(&mut self, loc: StmtLoc) -> &mut Self::Output {
+        &mut self.body[loc.block].statements[loc.statement]
+    }
+}
+
 /// Helper to construct a small ullbc body.
 pub struct BodyBuilder {
     /// The span to use for everything.

charon/src/bin/charon-driver/main.rs

@@ -11,7 +11,6 @@
 #![expect(incomplete_features)]
 #![feature(box_patterns)]
 #![feature(deref_patterns)]
-#![feature(if_let_guard)]
 #![feature(iter_array_chunks)]
 #![feature(iterator_try_collect)]
 #![feature(macro_metavar_expr)]