Update ML

Author: N1ark

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.169"
+let supported_charon_version = "0.1.170"

charon-ml/src/PrintExpressions.ml

@@ -222,6 +222,4 @@ and rvalue_to_string (env : 'a 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

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_GAstOfJson.ml

@@ -1760,10 +1760,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/Cargo.lock

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.169"
+version = "0.1.170"
 authors = [
     "Son Ho <hosonmarc@gmail.com>",
     "Guillaume Boisseau <nadrieril+git@gmail.com>",

charon/Cargo.toml

@@ -8,7 +8,7 @@
     rust-overlay = {
       # We pin a specific commit because we require a relatively recent version
       # and flake dependents don't look at our flake.lock.
-      url = "github:oxalica/rust-overlay/ab726555a9a72e6dc80649809147823a813fa95b";
+      url = "github:oxalica/rust-overlay/085bdbf5dde5477538e4c87d1684b6c6df56c0ad";
       inputs.nixpkgs.follows = "nixpkgs";
     };
     crane.url = "github:ipetkov/crane";