Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2

Complete the constants extraction by making all functions fail

1 files changed, 11 insertions, 16 deletions

diff --git a/src/Values.ml b/src/Values.ml
index 4e45db03..4585b443 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -6,13 +6,9 @@ open Types
  * inside abstractions) *)
 
 module VarId = IdGen ()
-
 module BorrowId = IdGen ()
-
 module SymbolicValueId = IdGen ()
-
 module AbstractionId = IdGen ()
-
 module FunCallId = IdGen ()
 
 (** A variable *)
@@ -83,13 +79,9 @@ type symbolic_value = {
 class ['self] iter_typed_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
-
     method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
-
     method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
-
     method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
-
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
   end
 
@@ -228,7 +220,6 @@ and typed_value = { value : value; ty : ety }
 class ['self] iter_typed_value =
   object (_self : 'self)
     inherit [_] iter_typed_value_visit_mvalue
-
     method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
   end
 
@@ -236,7 +227,6 @@ class ['self] iter_typed_value =
 class ['self] map_typed_value =
   object (_self : 'self)
     inherit [_] map_typed_value_visit_mvalue
-
     method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
   end
 
@@ -275,7 +265,6 @@ type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show]
 class ['self] iter_aproj_base =
   object (_self : 'self)
     inherit [_] iter_typed_value
-
     method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
 
     method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
@@ -286,7 +275,6 @@ class ['self] iter_aproj_base =
 class ['self] map_aproj_base =
   object (_self : 'self)
     inherit [_] map_typed_value
-
     method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
 
     method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
@@ -374,9 +362,7 @@ type region = RegionVarId.id Types.region [@@deriving show]
 class ['self] iter_typed_avalue_base =
   object (_self : 'self)
     inherit [_] iter_aproj
-
     method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> ()
-
     method visit_region : 'env -> region -> unit = fun _ _ -> ()
 
     method visit_abstract_shared_borrows
@@ -388,9 +374,7 @@ class ['self] iter_typed_avalue_base =
 class ['self] map_typed_avalue_base =
   object (_self : 'self)
     inherit [_] map_aproj
-
     method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id
-
     method visit_region : 'env -> region -> region = fun _ r -> r
 
     method visit_abstract_shared_borrows
@@ -798,6 +782,17 @@ type abs = {
           the symbolic AST, generated by the symbolic execution.
        *)
   kind : (abs_kind[@opaque]);
+  can_end : (bool[@opaque]);
+      (** Controls whether the region can be ended or not.
+          
+          This allows to "pin" some regions, and is useful when generating
+          backward functions.
+          
+          For instance, if we have: `fn f<'a, 'b>(...) -> (&'a mut T, &'b mut T)`,
+          when generating the backward function for 'a, we have to make sure we
+          don't need to end the return region for 'b (if it is the case, it means
+          the function doesn't borrow check).
+       *)
   parents : (AbstractionId.Set.t[@opaque]);  (** The parent abstractions *)
   original_parents : (AbstractionId.id list[@opaque]);
       (** The original list of parents, ordered. This is used for synthesis. *)