Start working on the generation of the symbolic AST

1 files changed, 28 insertions, 0 deletions

diff --git a/src/Values.ml b/src/Values.ml
index 4946b811..1812cd18 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -13,6 +13,10 @@ module SymbolicValueId = IdGen ()
 
 module AbstractionId = IdGen ()
 
+module FunCallId = IdGen ()
+
+module BackwardFunctionId = IdGen ()
+
 (** A variable *)
 
 type big_int = Z.t
@@ -712,6 +716,17 @@ type abs_kind =
 
 type abs = {
   abs_id : (AbstractionId.id[@opaque]);
+  call_id : (FunCallId.id[@opaque]);
+      (** The identifier of the function call which introduced this
+          abstraction. This is not used by the symbolic execution:
+          this is only used for pretty-printing and debugging, in the
+          symbolic AST, generated by the symbolic execution.
+       *)
+  back_id : (BackwardFunctionId.id option[@opaque]);
+      (** The id of the backward function to which this abstraction is linked.
+          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 *)
   regions : (RegionId.Set.t[@opaque]);  (** Regions owned by this abstraction *)
@@ -744,3 +759,16 @@ type abs = {
     In order to model the relations between the borrows, we use "abstraction values",
     which are a special kind of value.
 *)
+
+(** A symbolic expansion
+    
+    A symbolic expansion doesn't represent a value, but rather an operation
+    that we apply to values.
+    
+    TODO: this should rather be name "expanded_symbolic"
+ *)
+type symbolic_expansion =
+  | SeConcrete of constant_value
+  | SeAdt of (VariantId.id option * symbolic_value list)
+  | SeMutRef of BorrowId.id * symbolic_value
+  | SeSharedRef of BorrowId.Set.t * symbolic_value