Bump Charon

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-b1096182b418d99fa7440421dcf1099fda5785ae
+103daa06617306f28c2515e87efdcfc1a94dc7a2

src/PrePasses.ml

@@ -747,12 +747,8 @@ let remove_useless_joins (crate : crate) (f : fun_decl) : fun_decl =
             match rv with
             | Use _ | RvRef _ | RawPtr _ | NullaryOp _ | Aggregate _ ->
                 (can_inline, st :: ls)
-            | BinaryOp _
-            | UnaryOp _
-            | Discriminant _
-            | Len _
-            | Repeat _
-            | ShallowInitBox _ -> (false, st :: ls))
+            | BinaryOp _ | UnaryOp _ | Discriminant _ | Len _ | Repeat _ ->
+                (false, st :: ls))
         | SetDiscriminant _ | CopyNonOverlapping _ | Assert _ | Call _ | Error _
           -> (false, st :: ls))
   in

src/interp/InterpStatements.ml

@@ -847,9 +847,6 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
                 | Repeat _ ->
                     [%craise] st.span
                       "Repeat should have been removed in a micropass"
-                | ShallowInitBox _ ->
-                    [%craise] st.span
-                      "ShallowInitBox should have been removed in a micropass"
                 | Use _
                 | RvRef
                     ( _,

src/interp/InterpUtils.ml

@@ -447,8 +447,7 @@ let rvalue_get_place (rv : rvalue) : place option =
   | BinaryOp _
   | Discriminant _
   | Aggregate _
-  | Repeat _
-  | ShallowInitBox _ -> None
+  | Repeat _ -> None
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
 let symbolic_value_has_borrows span (ctx : eval_ctx) (sv : symbolic_value) :

src/llbc/FunsAnalysis.ml

@@ -120,8 +120,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) :
             | Len _
             | NullaryOp _
             | RawPtr _
-            | Repeat _
-            | ShallowInitBox _ -> ()
+            | Repeat _ -> ()
             | RvRef ({ kind = PlaceGlobal gref; _ }, _, _) -> (
                 (* A reference to a global: propagate can_fail.
 

tests/coq/demo/Demo.v

@@ -9,13 +9,13 @@ Local Open Scope Primitives_scope.
 Module Demo.
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2397:8-2397:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2456:8-2456:58
     Name pattern: [core::num::{u32}::wrapping_add]
     Visibility: public *)
 Axiom core_num_U32_wrapping_add : u32 -> u32 -> result u32.
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2434:8-2434:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2493:8-2493:58
     Name pattern: [core::num::{u32}::wrapping_sub]
     Visibility: public *)
 Axiom core_num_U32_wrapping_sub : u32 -> u32 -> result u32.

tests/fstar/demo/Demo.fst

@@ -6,13 +6,13 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2397:8-2397:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2456:8-2456:58
     Name pattern: [core::num::{u32}::wrapping_add]
     Visibility: public *)
 assume val core_num_U32_wrapping_add : u32 -> u32 -> result u32
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2434:8-2434:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2493:8-2493:58
     Name pattern: [core::num::{u32}::wrapping_sub]
     Visibility: public *)
 assume val core_num_U32_wrapping_sub : u32 -> u32 -> result u32

tests/lean/Derive.lean

@@ -25,7 +25,7 @@ namespace derive
 axiom Bool.Insts.CoreCmpPartialEqBool.ne : Bool → Bool → Result Bool
 
 /-- [alloc::boxed::{core::cmp::PartialEq<alloc::boxed::Box<T>> for alloc::boxed::Box<T>}::ne]:
-    Source: '/rustc/library/alloc/src/boxed.rs', lines 2056:4-2056:38
+    Source: '/rustc/library/alloc/src/boxed.rs', lines 2100:4-2100:38
     Name pattern: [alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne]
     Visibility: public -/
 @[rust_fun "alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne"]