summaryrefslogtreecommitdiff
path: root/src/test
diff options
context:
space:
mode:
Diffstat (limited to 'src/test')
-rw-r--r--src/test/pattern.sail24
-rw-r--r--src/test/run_tests.ml1
2 files changed, 25 insertions, 0 deletions
diff --git a/src/test/pattern.sail b/src/test/pattern.sail
new file mode 100644
index 00000000..35a6b632
--- /dev/null
+++ b/src/test/pattern.sail
@@ -0,0 +1,24 @@
+
+register nat n
+register nat x
+register nat y
+
+function unit main _ = {
+
+ (* works - x and y are set to 42 *)
+ n := 1;
+ y :=
+ (switch n {
+ case 0 -> { x := 21; x }
+ case 1 -> { x := 42; x }
+ case x -> { x := 99; x }
+ });
+
+ (* doesn't work - main returns 1 instead of 42 *)
+ n := 1;
+ switch n {
+ case 0 -> { 21 }
+ case 1 -> { 42 }
+ case x -> { 99 }
+ }
+}
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index a86e3d1c..df5598dc 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -2,6 +2,7 @@ let tests = [
"test1", Test1.defs;
"test2", Test2.defs;
"test3", Test3.defs;
+ "pattern", Pattern.defs;
"vectors", Vectors.defs;
] ;;