From 42da25ddae3deb8df125ca5d1963a0b40d683c2a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jan 2022 18:49:11 +0100
Subject: Make progress on SymbolicToPure.translate_end_abstraction

---
 src/Values.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src/Values.ml')

diff --git a/src/Values.ml b/src/Values.ml
index cc458bca..6378269f 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -737,12 +737,18 @@ type abs = {
           symbolic AST, generated by the symbolic execution.
        *)
   back_id : (RegionGroupId.id option[@opaque]);
-      (** The id of the backward function to which this abstraction is linked.
+      (** The id of the backward function to which this abstraction is linked,
+          if there is one. Note that it may not be the case, when introducing
+          abstractions to handle the input values for the function we are
+          synthesizing for instance. TODO: actually should never be None.
+          
           This is not used by the symbolic execution: it is a utility for
           the symbolic AST, generated by the symbolic execution.
        *)
   kind : (abs_kind[@opaque]);
   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. *)
   regions : (RegionId.Set.t[@opaque]);  (** Regions owned by this abstraction *)
   ancestors_regions : (RegionId.Set.t[@opaque]);
       (** Union of the regions owned by this abstraction's ancestors (not
-- 
cgit v1.2.3