summaryrefslogtreecommitdiff
path: root/compiler/SymbolicAst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SymbolicAst.ml')
-rw-r--r--compiler/SymbolicAst.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 528d8255..9d9adf4f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -77,6 +77,14 @@ type expression =
We use it to compute meaningful names for the variables we introduce,
to prettify the generated code.
*)
+ | ForwardEnd of expression
+ (** We use this delimiter to indicate at which point we switch to the
+ generation of code specific to the backward function(s).
+
+ TODO: use this to factorize the generation of the forward and backward
+ functions (today we replay the *whole* symbolic execution once per
+ generated function).
+ *)
| Meta of meta * expression (** Meta information *)
and expansion =