diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/Values.ml b/src/Values.ml index 95b1bd13..92b9df35 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -736,12 +736,13 @@ type abs = { this is only used for pretty-printing and debugging, in the 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, - 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. - + back_id : (RegionGroupId.id[@opaque]); + (** The region group id to which this abstraction is linked. + + In most situations, it gives the id of the backward function (hence + the name), but it is a bit more subtle in the case of synth input + and synth ret abstractions. + This is not used by the symbolic execution: it is a utility for the symbolic AST, generated by the symbolic execution. *) |