From 9f6ed55e4123f56c86925460d147707e8b0dc393 Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc_mak@outlook.com>
Date: Tue, 30 Jul 2024 13:55:00 +0100
Subject: [PATCH] Add broken proof example from Cerberus repo here

The test script in the Cerberus repo doesn't really have a good category
for "this is broken, but it should not be". Consequently, placing these
tests here makes more sense.
---
 src/example-archive/should-fail/README.md     |  3 ++-
 .../should-fail/working/c_sequencing_race.c   | 10 ++++++++++
 .../should-fail/working/letweak01.c           |  8 ++++++++
 .../broken/error-proof/self_ref_init.c        | 19 +++++++++++++++++++
 4 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 src/example-archive/should-fail/working/c_sequencing_race.c
 create mode 100644 src/example-archive/should-fail/working/letweak01.c
 create mode 100644 src/example-archive/simple-examples/broken/error-proof/self_ref_init.c

diff --git a/src/example-archive/should-fail/README.md b/src/example-archive/should-fail/README.md
index 49e793ab..7d639c08 100644
--- a/src/example-archive/should-fail/README.md
+++ b/src/example-archive/should-fail/README.md
@@ -1,2 +1,3 @@
 This folder contains deliberately incorrect proofs, which are intended to serve
-as negative test cases for CN. 
\ No newline at end of file
+as negative test cases for CN, i.e. the ones in `broken` are behaving as
+expected and the ones in `working` show a bug of permissiveness which needs fixing.
diff --git a/src/example-archive/should-fail/working/c_sequencing_race.c b/src/example-archive/should-fail/working/c_sequencing_race.c
new file mode 100644
index 00000000..c91abf15
--- /dev/null
+++ b/src/example-archive/should-fail/working/c_sequencing_race.c
@@ -0,0 +1,10 @@
+
+
+int
+f (int *x)
+/*@ requires take xv = Owned(x); @*/
+/*@ requires 0i32 <= xv && xv < 500i32; @*/
+/*@ ensures take xv2 = Owned(x); @*/
+{
+  return ((*x) + (*x));
+}
diff --git a/src/example-archive/should-fail/working/letweak01.c b/src/example-archive/should-fail/working/letweak01.c
new file mode 100644
index 00000000..be7d7fd6
--- /dev/null
+++ b/src/example-archive/should-fail/working/letweak01.c
@@ -0,0 +1,8 @@
+
+int
+f (int x) {
+  x = (x = 1);
+
+  return x + 2;
+}
+
diff --git a/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c b/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c
new file mode 100644
index 00000000..6195b3c9
--- /dev/null
+++ b/src/example-archive/simple-examples/broken/error-proof/self_ref_init.c
@@ -0,0 +1,19 @@
+
+/* based on a problematic example from linux kvm/pgtable.c */
+
+struct str {
+  int x;
+  int y;
+};
+
+int f (int x)
+/*@ requires (0i32 <= x) && (x < 200i32); @*/
+{
+  struct str str_inst = {
+    .x = x + 2,
+    .y = str_inst.x + 3,
+  };
+
+  return str_inst.y;
+}
+