diff options
| -rw-r--r-- | src/Interpreter.ml | 8 | ||||
| -rw-r--r-- | src/Print.ml | 5 |
2 files changed, 10 insertions, 3 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 75be6074..a49b2f3f 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -23,7 +23,8 @@ let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string let statement_to_string = Print.EvalCtxCfimAst.statement_to_string -let expression_to_string = Print.EvalCtxCfimAst.expression_to_string +let expression_to_string ctx = + Print.EvalCtxCfimAst.expression_to_string ctx " " " " (* TODO: move *) let mk_unit_ty : T.ety = T.Tuple [] @@ -2367,6 +2368,11 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector) } in + (* Put the (uninitialized) local variables *) + let ctx = + C.ctx_push_uninitialized_vars ctx (V.VarId.vector_to_list fdef.A.locals) + in + (* Evaluate the function *) let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in match eval_function_body config ctx fdef.A.body with diff --git a/src/Print.ml b/src/Print.ml index 57d9be0f..b9d7372c 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -909,7 +909,8 @@ module EvalCtxCfimAst = struct let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.statement_to_string fmt s - let expression_to_string (ctx : C.eval_ctx) (e : A.expression) : string = + let expression_to_string (ctx : C.eval_ctx) (indent : string) + (indent_incr : string) (e : A.expression) : string = let fmt = PA.eval_ctx_to_ast_formatter ctx in - PA.expression_to_string fmt "" " " e + PA.expression_to_string fmt indent indent_incr e end |