summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Identifiers.ml4
-rw-r--r--src/Interpreter.ml32
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 ()