diff options
Diffstat (limited to '')
-rw-r--r-- | src/Interpreter.ml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b8943a9a..3b16a1e3 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,6 +1,7 @@ open Types open Values open Expressions +open CfimAst open Print.Values open Errors @@ -28,6 +29,25 @@ type config = { mode : interpreter_mode; check_invariants : bool } type outer_borrows = Borrows of BorrowId.Set.t | Borrow of BorrowId.id +type stack_frame = { vars : var VarId.vector } +(** A function frame + + When using the interpreter in concrete mode (i.e, non symbolic) we + push a function frame whenever we enter a function body (and pop it + upon leaving it). + *) + +type eval_ctx = { + type_context : type_def TypeDefId.vector; + fun_context : fun_def FunDefId.vector; + type_vars : type_var TypeVarId.vector; + frames : stack_frame list; + env : env; + symbolic_counter : SymbolicValueId.generator; + borrows_counter : BorrowId.generator; +} +(** Evaluation context *) + (** The following type identifies the relative position of expressions (in particular borrows) in other expressions. |