diff options
Diffstat (limited to 'compiler/SymbolicAst.ml')
| -rw-r--r-- | compiler/SymbolicAst.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 7f682c9c..0e68d2fd 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -216,6 +216,11 @@ and loop = { input_svalues : V.symbolic_value list; (** The input symbolic values *) fresh_svalues : V.symbolic_value_id_set; (** The symbolic values introduced by the loop fixed-point *) + rg_to_given_back_tys : + ((T.RegionId.Set.t * T.rty list) T.RegionGroupId.Map.t[@opaque]); + (** The map from region group ids to the types of the values given back + by the corresponding loop abstractions. + *) end_expr : expression; (** The end of the function (upon the moment it enters the loop) *) loop_expr : expression; (** The symbolically executed loop body *) |