From 15309c879d2c877953512c401e66a7a48af6df97 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 19 Sep 2017 17:00:05 +0100
Subject: Added additional case for tuple l-expressions to increase
 compatability for ASL.

---
 test/typecheck/pass/nzcv.sail | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test/typecheck/pass/nzcv.sail

(limited to 'test/typecheck')

diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
new file mode 100644
index 00000000..a477cd97
--- /dev/null
+++ b/test/typecheck/pass/nzcv.sail
@@ -0,0 +1,9 @@
+default Order dec
+
+val bit[4] -> unit effect pure test
+
+function test nzcv =
+{
+  (N,Z,C,V) := nzcv;
+  ()
+}
-- 
cgit v1.2.3


From 381a3967ebd9269082b452669f507787decf28b0 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 27 Sep 2017 15:23:43 +0100
Subject: Add while-loops to Lem backend

---
 test/typecheck/pass/while_MM.sail | 23 +++++++++++++++++++++++
 test/typecheck/pass/while_MP.sail | 17 +++++++++++++++++
 test/typecheck/pass/while_PM.sail | 23 +++++++++++++++++++++++
 test/typecheck/pass/while_PP.sail | 24 ++++++++++++++++++++++++
 4 files changed, 87 insertions(+)
 create mode 100644 test/typecheck/pass/while_MM.sail
 create mode 100644 test/typecheck/pass/while_MP.sail
 create mode 100644 test/typecheck/pass/while_PM.sail
 create mode 100644 test/typecheck/pass/while_PP.sail

(limited to 'test/typecheck')

diff --git a/test/typecheck/pass/while_MM.sail b/test/typecheck/pass/while_MM.sail
new file mode 100644
index 00000000..e6916edd
--- /dev/null
+++ b/test/typecheck/pass/while_MM.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
+val extern (int, int) -> int effect pure add_int = "add"
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int
+overload (deinfix +) [add_vec_int; add_range; add_int]
+
+val extern bool -> bool effect pure bool_not = "not"
+
+val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,dec,bit> effect pure cast_0_vec_dec
+
+register (bit[64]) COUNT
+register (bool) INT
+
+function (unit) test () = {
+  COUNT := 0;
+  while (bool_not(INT)) do {
+    COUNT := COUNT + 1;
+  }
+}
+
diff --git a/test/typecheck/pass/while_MP.sail b/test/typecheck/pass/while_MP.sail
new file mode 100644
index 00000000..05d396e2
--- /dev/null
+++ b/test/typecheck/pass/while_MP.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val extern (int, int) -> int effect pure add_int = "add"
+overload (deinfix +) [add_vec_int; add_range; add_int]
+
+val extern bool -> bool effect pure bool_not = "not"
+
+register (bool) INT
+
+function (int) test () = {
+  (int) count := 0;
+  while (bool_not(INT)) do {
+    count := count + 1;
+  };
+  return count;
+}
+
diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail
new file mode 100644
index 00000000..b03a87dc
--- /dev/null
+++ b/test/typecheck/pass/while_PM.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt"
+val extern (int, int) -> bool effect pure lt_int = "lt"
+overload (deinfix <) [lt_range_atom; lt_int]
+
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
+val extern (int, int) -> int effect pure add_int = "add"
+overload (deinfix +) [add_range; add_int]
+
+val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, int) -> bit effect pure vector_access = "bitvector_access_dec"
+
+register (bit[64]) GPR00
+
+function (unit) test ((bit) b) = {
+  (int) i := 0;
+  while (i < 64) do {
+    GPR00[i] := b;
+    i := i + 1;
+  }
+}
+
diff --git a/test/typecheck/pass/while_PP.sail b/test/typecheck/pass/while_PP.sail
new file mode 100644
index 00000000..454cc9ac
--- /dev/null
+++ b/test/typecheck/pass/while_PP.sail
@@ -0,0 +1,24 @@
+default Order dec
+
+val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt"
+val extern (int, int) -> bool effect pure lt_int = "lt"
+overload (deinfix <) [lt_range_atom; lt_int]
+
+val (int, int) -> int effect pure mult_int
+overload (deinfix * ) [mult_int]
+
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
+val extern (int, int) -> int effect pure add_int = "add"
+overload (deinfix +) [add_range; add_int]
+
+function (int) test ((int) n) = {
+  (int) i := 1;
+  (int) j := 1;
+  while (i < n) do {
+    j := i * j;
+    i := i + 1;
+  };
+  j
+}
+
-- 
cgit v1.2.3