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

@@ -1,2 +1,3 @@
 This folder contains deliberately incorrect proofs, which are intended to serve
-as negative test cases for CN. 
+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.

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));
+}

src/example-archive/should-fail/working/letweak01.c

@@ -0,0 +1,8 @@
+
+int
+f (int x) {
+  x = (x = 1);
+
+  return x + 2;
+}
+

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;
+}
+