Update 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.
-ac5539d88128755c32da28ed78884fe899afe452
+af5e49f331165e63ca25071f2335da38815fc1e9

src/interp/InterpreterBorrowsCore.ml

@@ -1467,7 +1467,6 @@ let rec norm_proj_tys_union (span : Meta.span) (ty1 : rty) (ty2 : rty) : rty =
   | TTraitType (tr1, item1), TTraitType (tr2, item2) ->
       sanity_check __FILE__ __LINE__ (item1 = item2) span;
       TTraitType (norm_proj_trait_refs_union span tr1 tr2, item1)
-  | TDynTrait (), TDynTrait () -> TDynTrait ()
   | ( TFnPtr
         { binder_regions = binder_regions1; binder_value = inputs1, output1 },
       TFnPtr

src/llbc/Contexts.ml

@@ -7,13 +7,13 @@ open ValuesUtils
 open Errors
 include ContextsBase
 
-module OrderedBinder : Collections.OrderedType with type t = binder = struct
-  type t = binder
+module OrderedBinder : Collections.OrderedType with type t = var_binder = struct
+  type t = var_binder
 
-  let compare x y = compare_binder x y
-  let to_string x = show_binder x
-  let pp_t fmt x = Format.pp_print_string fmt (show_binder x)
-  let show_t x = show_binder x
+  let compare x y = compare_var_binder x y
+  let to_string x = show_var_binder x
+  let pp_t fmt x = Format.pp_print_string fmt (show_var_binder x)
+  let show_t x = show_var_binder x
 end
 
 module BinderMap = Collections.MakeMap (OrderedBinder)
@@ -104,7 +104,7 @@ let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
 
 (** Lookup a variable in the current frame *)
 let env_lookup_var (span : Meta.span) (env : env) (vid : LocalId.id) :
-    var_binder * typed_value =
+    real_var_binder * typed_value =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
@@ -120,8 +120,8 @@ let env_lookup_var (span : Meta.span) (env : env) (vid : LocalId.id) :
   in
   lookup env
 
-let ctx_lookup_var_binder (span : Meta.span) (ctx : eval_ctx) (vid : LocalId.id)
-    : var_binder =
+let ctx_lookup_real_var_binder (span : Meta.span) (ctx : eval_ctx)
+    (vid : LocalId.id) : real_var_binder =
   fst (env_lookup_var span ctx.env vid)
 
 let ctx_lookup_type_decl (span : Meta.span) (ctx : eval_ctx)
@@ -183,7 +183,7 @@ let env_update_var_value (span : Meta.span) (env : env) (vid : LocalId.id)
   in
   update env
 
-let var_to_binder (var : local) : var_binder =
+let var_to_binder (var : local) : real_var_binder =
   { index = var.index; name = var.name }
 
 (** Update a variable's value in an evaluation context.

src/llbc/ContextsBase.ml

@@ -139,18 +139,18 @@ class ['self] map_env_base =
   end
 
 (** A binder used in an environment, to map a variable to a value *)
-type var_binder = {
+type real_var_binder = {
   index : local_id;  (** Unique variable identifier *)
   name : string option;  (** Possible name *)
 }
 
 (** A binder, for a "real" variable or a dummy variable *)
-and binder = BVar of var_binder | BDummy of dummy_var_id
+and var_binder = BVar of real_var_binder | BDummy of dummy_var_id
 
 (** Environment value: mapping from variable to value, abstraction (only used in
     symbolic mode) or stack frame delimiter. *)
 and env_elem =
-  | EBinding of binder * typed_value
+  | EBinding of var_binder * typed_value
       (** Variable binding - the binder is None if the variable is a dummy
           variable (we use dummy variables to store temporaries while doing
           bookkeeping such as ending borrows for instance). *)

src/llbc/Print.ml

@@ -419,25 +419,26 @@ end
 module Contexts = struct
   open Values
 
-  let var_binder_to_string (env : fmt_env) (bv : var_binder) : string =
+  let real_var_binder_to_string (env : fmt_env) (bv : real_var_binder) : string
+      =
     match bv.name with
     | None -> local_id_to_string env bv.index
     | Some name -> name ^ "^" ^ LocalId.to_string bv.index
 
   let dummy_var_id_to_string (bid : DummyVarId.id) : string =
     "_@" ^ DummyVarId.to_string bid
 
-  let binder_to_string (env : fmt_env) (bv : binder) : string =
+  let var_binder_to_string (env : fmt_env) (bv : var_binder) : string =
     match bv with
-    | BVar b -> var_binder_to_string env b
+    | BVar b -> real_var_binder_to_string env b
     | BDummy bid -> dummy_var_id_to_string bid
 
   let env_elem_to_string ?(span : Meta.span option = None) (env : fmt_env)
       (verbose : bool) (with_var_types : bool) (indent : string)
       (indent_incr : string) (ev : env_elem) : string =
     match ev with
     | EBinding (var, tv) ->
-        let bv = binder_to_string env var in
+        let bv = var_binder_to_string env var in
         let ty =
           if with_var_types then " : " ^ ty_to_string env tv.ty else ""
         in

src/symbolic/SymbolicAst.ml

@@ -16,7 +16,7 @@ open LlbcAst
     information, etc.). We later use this place information to generate
     meaningful name, to prettify the generated code. *)
 type mplace =
-  | PlaceLocal of Contexts.var_binder
+  | PlaceLocal of Contexts.real_var_binder
       (** It is important that we store the binder, and not just the variable
           id, because the most important information in a place is the name of
           the variable! *)
@@ -90,7 +90,6 @@ class ['self] iter_expression_base =
 
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
     method visit_espan : 'env -> espan -> unit = fun _ _ -> ()
-    method visit_span : 'env -> Meta.span -> unit = fun _ _ -> ()
 
     method visit_region_group_id_map :
         'a. ('env -> 'a -> unit) -> 'env -> 'a region_group_id_map -> unit =

src/symbolic/SynthesizeSymbolic.ml

@@ -11,7 +11,7 @@ let mk_mplace (span : Meta.span) (p : place) (ctx : Contexts.eval_ctx) : mplace
   let rec place_to_mplace (place : place) : mplace =
     match place.kind with
     | PlaceLocal var_id ->
-        PlaceLocal (Contexts.ctx_lookup_var_binder span ctx var_id)
+        PlaceLocal (Contexts.ctx_lookup_real_var_binder span ctx var_id)
     | PlaceProjection (subplace, pe) ->
         PlaceProjection (place_to_mplace subplace, pe)
   in