summaryrefslogtreecommitdiff
path: root/src/test
diff options
context:
space:
mode:
Diffstat (limited to 'src/test')
-rw-r--r--src/test/run_tests.ml1
-rw-r--r--src/test/test3.sail16
2 files changed, 17 insertions, 0 deletions
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index 58ea2b17..f1956b1e 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -1,6 +1,7 @@
let tests = [
"test1", Test1.defs;
"test2", Test2.defs;
+ "test3", Test3.defs;
] ;;
let run_all () = List.iter Run_interp.run tests ;;
diff --git a/src/test/test3.sail b/src/test/test3.sail
new file mode 100644
index 00000000..36952bf7
--- /dev/null
+++ b/src/test/test3.sail
@@ -0,0 +1,16 @@
+(* a register containing nat numbers *)
+register nat reg
+(* a function to read from memory; wmem serves no purpose currently,
+ memory-writing functions are figured out syntactically. *)
+val ( nat -> nat effect { wmem , rmem } ) MEM
+
+function nat main _ = {
+ (* memory read, thanks to effect { rmem} above *)
+ MEM(0);
+ (* left-hand side function call = memory write *)
+ MEM(0) := 1;
+ (* register read, thanks to register declaration *)
+ reg;
+ (* register write, idem *)
+ reg := 1;
+}