From 731c4d23661f16fab423daf8f88ed69f0b3a0205 Mon Sep 17 00:00:00 2001
From: Zain Aamer <ZippeyKeys12@gmail.com>
Date: Fri, 26 Jul 2024 19:38:27 -0400
Subject: [PATCH] [CN-Test-Gen] Add failing examples to CI

---
 tests/cn-test-gen/src/abs.fail.c      | 12 ++++
 tests/cn-test-gen/src/abs_mem.fail.c  | 16 ++++++
 tests/cn-test-gen/src/list_rev.fail.c | 79 +++++++++++++++++++++++++++
 3 files changed, 107 insertions(+)
 create mode 100644 tests/cn-test-gen/src/abs.fail.c
 create mode 100644 tests/cn-test-gen/src/abs_mem.fail.c
 create mode 100644 tests/cn-test-gen/src/list_rev.fail.c

diff --git a/tests/cn-test-gen/src/abs.fail.c b/tests/cn-test-gen/src/abs.fail.c
new file mode 100644
index 000000000..da0b4c592
--- /dev/null
+++ b/tests/cn-test-gen/src/abs.fail.c
@@ -0,0 +1,12 @@
+int abs(int x)
+/*@ requires MINi32() < x;
+    ensures return == ((x >= 0i32) ? x : (0i32-x));
+@*/
+{
+  if (x >= 0) {
+    return x;
+  }
+  else {
+    return x;
+  }
+}
diff --git a/tests/cn-test-gen/src/abs_mem.fail.c b/tests/cn-test-gen/src/abs_mem.fail.c
new file mode 100644
index 000000000..c253f7f06
--- /dev/null
+++ b/tests/cn-test-gen/src/abs_mem.fail.c
@@ -0,0 +1,16 @@
+int abs_mem(int* p)
+/*@ requires take x = Owned<int>(p);
+             MINi32() < x;
+    ensures take x2 = Owned<int>(p);
+            x == x2;
+            return == ((x >= 0i32) ? x : (0i32-x));
+@*/
+{
+  int x = *p;
+  if (x >= 0) {
+    return x;
+  }
+  else {
+    return x;
+  }
+}
diff --git a/tests/cn-test-gen/src/list_rev.fail.c b/tests/cn-test-gen/src/list_rev.fail.c
new file mode 100644
index 000000000..8802a927b
--- /dev/null
+++ b/tests/cn-test-gen/src/list_rev.fail.c
@@ -0,0 +1,79 @@
+struct int_list {
+  int head;
+  struct int_list* tail;
+};
+
+/*@
+datatype seq {
+  Seq_Nil {},
+  Seq_Cons {i32 head, datatype seq tail}
+}
+
+predicate (datatype seq) IntList(pointer p) {
+  if (is_null(p)) {
+    return Seq_Nil{};
+  } else {
+    take H = Owned<struct int_list>(p);
+    take tl = IntList(H.tail);
+    return (Seq_Cons { head: H.head, tail: tl });
+  }
+}
+
+function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
+  match xs {
+    Seq_Nil {} => {
+      ys
+    }
+    Seq_Cons {head : h, tail : zs}  => {
+      Seq_Cons {head: h, tail: append(zs, ys)}
+    }
+  }
+}
+
+function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {
+  match xs {
+    Seq_Nil {} => {
+      Seq_Cons {head: y, tail: Seq_Nil{}}
+    }
+    Seq_Cons {head: x, tail: zs}  => {
+      Seq_Cons{head: x, tail: snoc (zs, y)}
+    }
+  }
+}
+
+function [rec] (datatype seq) rev(datatype seq xs) {
+  match xs {
+    Seq_Nil {} => {
+      Seq_Nil {}
+    }
+    Seq_Cons {head : h, tail : zs}  => {
+      snoc (rev(zs), h)
+    }
+  }
+}
+@*/
+
+struct int_list* IntList_rev_aux(struct int_list* xs, struct int_list* ys)
+  /*@ requires take L1 = IntList(xs); @*/
+  /*@ requires take L2 = IntList(ys); @*/
+  /*@ ensures take R = IntList(return); @*/
+  /*@ ensures R == append(rev(L2), L1); @*/
+{
+  if (ys == 0) {
+    return xs;
+  }
+  else {
+    struct int_list* tmp = ys->tail;
+    ys->head = -1;
+    ys->tail = xs;
+    return IntList_rev_aux(ys, tmp);
+  }
+}
+
+struct int_list* IntList_rev(struct int_list* xs)
+  /*@ requires take L1 = IntList(xs); @*/
+  /*@ ensures take L1_rev = IntList(return); @*/
+  /*@ ensures L1_rev == rev(L1); @*/
+{
+  return IntList_rev_aux(0, xs);
+}