diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 28 |
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 |