diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Identifiers.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 32 |
2 files changed, 36 insertions, 0 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 824fd8ad..8072b316 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -16,6 +16,8 @@ module type Id = sig val zero : id + val generator_zero : generator + val fresh : generator -> id * generator val to_string : id -> string @@ -85,6 +87,8 @@ module IdGen () : Id = struct let zero = 0 + let generator_zero = 0 + let incr x = (* Identifiers should never overflow (because max_int is a really big * value - but we really want to make sure we detect overflows if diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 308a443b..66eb7d87 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2307,3 +2307,35 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : | None -> eval_expression config ctx1 otherwise | Some (_, tgt) -> eval_expression config ctx1 tgt) | _ -> failwith "Inconsistent state")) + +(** Test a unit function (taking no arguments) by evaluating it in an empty + environment + *) +let test_unit_function (type_decls : T.type_def T.TypeDefId.vector) + (fun_decls : A.fun_def A.FunDefId.vector) (fid : A.FunDefId.id) : + unit eval_result = + (* Retrieve the function declaration *) + let fdef = A.FunDefId.nth fun_decls fid in + + (* Sanity check - *) + assert (T.RegionVarId.length fdef.A.signature.region_params = 0); + assert (T.TypeVarId.length fdef.A.signature.type_params = 0); + assert (fdef.A.arg_count = 0); + + (* Create the evaluation context *) + let ctx = + { + C.type_context = type_decls; + C.fun_context = fun_decls; + C.type_vars = T.TypeVarId.empty_vector; + C.env = []; + C.symbolic_counter = V.SymbolicValueId.generator_zero; + C.borrow_counter = V.BorrowId.generator_zero; + } + 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 + | Error err -> Error err + | Ok _ -> Ok () |