+1 test

rems-project · Sep 12, 2023 · b2a10c9 · b2a10c9
1 parent 57e524d
commit b2a10c9
Showing 1 changed file with 22 additions and 0 deletions.
diff --git a/tests/cn/incomplete_match.error.c b/tests/cn/incomplete_match.error.c
@@ -0,0 +1,22 @@
+
+/*@
+datatype mylist {
+  Nil {},
+  Cons {integer hd, datatype mylist tl}
+}
+
+function (integer) snd (datatype mylist t) {
+  match t {
+    Cons {hd: _, tl: Cons {hd: v, tl: _}} => { v }
+    Nil {} => { 0 }
+  }
+}
+@*/
+
+void
+check_foo (int x)
+/*@ ensures snd(Cons {hd: 10, tl: Cons {hd: 20, tl: Nil {}}}) == 20 @*/
+{
+}
+
+