8 files changed, 97 insertions, 0 deletions
diff --git a/test/c/zero_length_bv.expect b/test/c/zero_length_bv.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/zero_length_bv.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/zero_length_bv.sail b/test/c/zero_length_bv.sail
new file mode 100644
index 00000000..332b8aae
--- /dev/null
+++ b/test/c/zero_length_bv.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let x: bits(0) = [];
+  if x == sail_zeros(0) then {
+    print_endline("ok")
+  };
+  let x: vector(0, dec, string) = [];
+  ()
+}
+\ No newline at end of file
diff --git a/test/coq/pass/while_MM_terminating.sail b/test/coq/pass/while_MM_terminating.sail
new file mode 100644
index 00000000..e3bca7f5
--- /dev/null
+++ b/test/coq/pass/while_MM_terminating.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+register COUNT : int
+
+register INT : bool
+
+function test () -> unit = {
+  COUNT = 0;
+  while not_bool(INT) do {
+    COUNT = COUNT + 1;
+    if COUNT > 5 then
+      INT = true
+  }
+}
+
+termination_measure test while (5 - COUNT)
diff --git a/test/coq/pass/while_MP_terminating.sail b/test/coq/pass/while_MP_terminating.sail
new file mode 100644
index 00000000..d9b71ad9
--- /dev/null
+++ b/test/coq/pass/while_MP_terminating.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+register INT : bool
+
+function test () -> int = {
+  count : int = 0;
+  while not_bool(INT) & count < 5 do count = count + 1;
+  return(count)
+}
+
+termination_measure test while 5 - count
diff --git a/test/coq/pass/while_PM_terminating.sail b/test/coq/pass/while_PM_terminating.sail
new file mode 100644
index 00000000..5129e997
--- /dev/null
+++ b/test/coq/pass/while_PM_terminating.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+register GPR00 : int
+
+function test b : int -> unit = {
+  i : int = 0;
+  while i < 64 do {
+    GPR00 = b + i;
+    i = i + 1;
+  }
+}
+
+termination_measure test while 64 - i
diff --git a/test/coq/pass/while_PP_terminating.sail b/test/coq/pass/while_PP_terminating.sail
new file mode 100644
index 00000000..00a4450b
--- /dev/null
+++ b/test/coq/pass/while_PP_terminating.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+function test n : int -> int = {
+  i : int = 1;
+  j : int = 1;
+  while i < n do {
+    j = i * j;
+    i = i + 1
+  };
+  j
+}
diff --git a/test/coq/skip b/test/coq/skip
index 49744fce..a4be9719 100644
--- a/test/coq/skip
+++ b/test/coq/skip
@@ -42,3 +42,12 @@ reg_mod.sail
 reg_ref.sail
 XXXXX Dodgy division/modulo stuff
 Replicate.sail
+XXXXX Non-terminating loops - I've written terminating versions of these
+while_MM.sail
+while_MP.sail
+while_PM.sail
+while_PP.sail
+XXXXX Not yet - haven't decided whether to support register reads in measures
+while_MM_terminating.sail
+XXXXX Not yet - haven't arranged for lifting pure loops into the monad (or proving termination outright) yet
+while_PP_terminating.sail
diff --git a/test/typecheck/pass/zero_length_bv.sail b/test/typecheck/pass/zero_length_bv.sail
new file mode 100644
index 00000000..332b8aae
--- /dev/null
+++ b/test/typecheck/pass/zero_length_bv.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let x: bits(0) = [];
+  if x == sail_zeros(0) then {
+    print_endline("ok")
+  };
+  let x: vector(0, dec, string) = [];
+  ()
+}
+\ No newline at end of file