Add a few negative examples

src/example-archive/README.md

@@ -9,6 +9,7 @@ This directory contains examples for CN. Each subdirectory contains examples fro
   [here](https://dafny.org/dafny/OnlineTutorial/guide.html).
 * `Rust` - C versions of Rust programs, with CN annotations that provide the same guarantees as the Rust type-checker.
 * `SAW` - Examples derived from the [Software Analysis Workbench (SAW)](https://saw.galois.com) repository and tutorial. 
+* `should-fail` - Small examples that should always fail. 
 * `open-sut` - Examples inspired by the VERSE Open System Under Test (Open SUT).
 
 ## Organization  

src/example-archive/check-all.sh

@@ -12,7 +12,7 @@ subdirs=(
   "c-testsuite" 
   "dafny-tutorial" 
   "java_program_verification_challenges" 
-  "negative-examples"
+  "should-fail"
   "open-sut"
   "Rust" 
   "SAW" 

src/example-archive/should-fail/README.md

@@ -0,0 +1,2 @@
+This folder contains deliberately incorrect proofs, which are intended to serve
+as negative test cases for CN. 

src/example-archive/should-fail/broken/error-proof/arith_neg_1.c

@@ -0,0 +1,9 @@
+// Negative test case: proof should fail 
+
+// The specification claims the function returns a non-zero value, but the
+// implementation returns zero.
+int arith_neg_1() 
+/*@ ensures return != 0i32; @*/
+{
+  return 0; 
+}

src/example-archive/should-fail/broken/error-proof/memory_neg_1.c

@@ -0,0 +1,8 @@
+// Negative test case: proof should fail 
+
+// The implementation writes to memory location *p, but this location is not
+// included in the specification  
+void memory_neg_1( int *p )
+{
+  *p = 1; 
+}

src/example-archive/should-fail/broken/error-proof/overflow_neg_1.c

@@ -0,0 +1,9 @@
+// Negative test case: proof should fail 
+
+// The precondition constraints i to be the maximum allowed value of an i32. The
+// function increments this value, which overflows the value and causes UB 
+void overflow_neg_1(int i) 
+/*@ requires i == MAXi32(); @*/
+{
+  i = i + 1; 
+}

src/example-archive/should-fail/broken/error-proof/overflow_neg_2.c

@@ -0,0 +1,9 @@
+// Negative test case: proof should fail 
+
+// The precondition constraints i to be the minimum allowed value of an i32. The
+// function decrements this value, which overflows the value and causes UB 
+void overflow_neg_2(int i) 
+/*@ requires i == MINi32(); @*/
+{
+  i = i - 1; 
+}

src/example-archive/should-fail/broken/error-proof/ownership_neg_1.c

@@ -0,0 +1,10 @@
+// Negative test case: proof should fail 
+
+// Precondition includes access to the resource Owned(p), which disappears in
+// the postcondition 
+void ownership_neg_1(int *p) 
+/*@ requires take P = Owned(p); @*/
+/*@ ensures true; @*/
+{
+  ; 
+}

src/example-archive/should-fail/broken/error-proof/ownership_neg_2.c

@@ -0,0 +1,10 @@
+// Negative test case: proof should fail 
+
+// Precondition takes ownership of no resources, but then the postcondition
+// claims ownership of Owned(p)  
+void ownership_neg_2(int *p) 
+/*@ requires true; @*/
+/*@ ensures take P_ = Owned(p); @*/
+{
+  ; 
+}

src/example-archive/should-fail/broken/error-proof/ownership_neg_3.c

@@ -0,0 +1,12 @@
+// Negative test case: proof should fail 
+
+// Precondition includes access to the resource Owned(p), which is duplicated in
+// the postcondition  
+void ownership_neg_3(int *p) 
+/*@ requires take P = Owned(p); @*/
+/*@ ensures 
+      take P_ = Owned(p); 
+      take Q_ = Owned(p); @*/
+{
+  ; 
+}

src/example-archive/should-fail/broken/error-proof/trivial_neg_1.c

@@ -0,0 +1,8 @@
+// Negative test case: proof should fail 
+
+// The specification has a false postcondition 
+void trivial_neg_1() 
+/*@ ensures false; @*/
+{
+  ; 
+}

src/example-archive/simple-examples/broken/error-proof/ownership_1.c

@@ -0,0 +1,16 @@
+// This example should be provable because Owned locations should be 
+// disjoint. But CN currently doesn't enforce this property. 
+// See: https://github.com/rems-project/cerberus/issues/295 
+
+void ownership_1(int *a, int *b)
+/*@ 
+requires 
+  take P1 = Owned(a); 
+  take P2 = Owned(b);
+ensures 
+  a != b; 
+@*/
+{
+  /*@ split_case a == b; @*/
+  ; 
+}