summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/InterpreterStatements.ml1
-rw-r--r--src/SymbolicToPure.ml8
-rw-r--r--src/Values.ml13
3 files changed, 10 insertions, 12 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 59d2c4da..83ad13fe 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -672,7 +672,6 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
let create_abs (back_id : T.RegionGroupId.id) (rg : A.abs_region_group) :
V.abs =
let abs_id = rg.T.id in
- let back_id = Some back_id in
let original_parents = rg.parents in
let parents =
List.fold_left
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 60fc8c7c..06ccf7bf 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -220,7 +220,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx * fun_id
=
(* Insert the abstraction in the call informations *)
- let back_id = Option.get abs.back_id in
+ let back_id = abs.back_id in
let info = V.FunCallId.Map.find abs.call_id ctx.calls in
assert (not (T.RegionGroupId.Map.mem back_id info.backwards));
let backwards = T.RegionGroupId.Map.add back_id abs info.backwards in
@@ -233,7 +233,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx * fun_id
(* Retrieve the fun_id *)
let fun_id =
match info.forward.call_id with
- | S.Fun (fid, _) -> Regular (fid, Some (Option.get abs.back_id))
+ | S.Fun (fid, _) -> Regular (fid, Some abs.back_id)
| S.Unop _ | S.Binop _ -> failwith "Unreachable"
in
(* Update the context and return *)
@@ -669,9 +669,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
* *)
(* First, retrieve the list of variables used for the inputs for the
* backward function *)
- let inputs =
- T.RegionGroupId.Map.find (Option.get abs.back_id) ctx.backward_inputs
- in
+ let inputs = T.RegionGroupId.Map.find abs.back_id ctx.backward_inputs in
raise Unimplemented
and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
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.
*)