diff options
Diffstat (limited to 'src/Values.ml')
| -rw-r--r-- | src/Values.ml | 8 |
1 files changed, 7 insertions, 1 deletions
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 |