Make the back_id field non optional in Values.abs

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.
        *)