Merge remote-tracking branch 'origin/main' into son/implicit

AeneasVerif · Sep 9, 2024 · 53dbdf8 · 53dbdf8
2 parents 6553c6b + 3f74062
commit 53dbdf8
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 9 deletions.
diff --git a/charon-pin b/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.
-96448ed72c9e8838ca2ed6b8477b5f2fb9cc8058
+92a3a80cb9283f018498cd81ce9c5bb94c73b8bd
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
@@ -143,7 +143,7 @@ let rec access_projection (span : Meta.span) (access : projection_access)
           (* Expand the symbolic value *)
           Error (FailSymbolic (1 + List.length p', sp))
       (* Box dereferencement *)
-      | ( DerefBox,
+      | ( Deref,
           VAdt { variant_id = None; field_values = [ bv ] },
           TAdt (TAssumed TBox, _) ) -> (
           (* We allow moving outside of boxes. In practice, this kind of

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
@@ -1879,7 +1879,7 @@ let abs_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) :
 let translate_mprojection_elem (pe : E.projection_elem) :
     mprojection_elem option =
   match pe with
-  | Deref | DerefBox -> None
+  | Deref -> None
   | Field (pkind, field_id) -> Some { pkind; field_id }
 
 let translate_mprojection (p : E.projection) : mprojection =

diff --git a/flake.lock b/flake.lock