diff options
Diffstat (limited to 'compiler/SymbolicAst.ml')
-rw-r--r-- | compiler/SymbolicAst.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 9d95db7f..b0e4735a 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -91,8 +91,15 @@ type expression = function, the map from region group ids to expressions gives the end of the translation for the backward functions. *) + | Loop of loop | Meta of meta * expression (** Meta information *) +and loop = { + end_expr : expression; + (** The end of the function (upon the moment it enters the loop) *) + loop_expr : expression; (** The symbolically executed loop body *) +} + and expansion = | ExpandNoBranch of V.symbolic_expansion * expression (** A symbolic expansion which doesn't generate a branching. |