Add a few more small examples and error cases (#29)

src/example-archive/simple-examples/broken/error-cerberus/pred_1.c

@@ -0,0 +1,24 @@
+// An example of defining a simple CN predicate. Broken as of 2024-7-4 thanks
+// to a CN parsing issue. See: https://github.com/rems-project/cerberus/issues/266
+
+/*@ 
+predicate (i32) TestMemoryEqZero_1(pointer p) {
+ take PVal = Owned<int>(p); 
+ if (PVal == 0i32) {
+ return 1i32; 
+ } else {
+ return 0i32; 
+ }
+}
+@*/
+
+void pred_1(int *p) 
+/*@ requires 
+ take PreP = Owned<int>(p); 
+ PreP == 0i32; @*/
+/*@ ensures 
+ take TestP = TestMemoryEqZero_1(p); 
+ TestP == 1i32; @*/
+{ 
+ ; 
+}

src/example-archive/simple-examples/broken/error-crash/array_crash_2.c

@@ -1 +1,4 @@
+// Examples of failed array initialization. 
+// See: https://github.com/rems-project/cerberus/issues/253
+
 void a() { ({}); }

src/example-archive/simple-examples/broken/error-crash/array_crash_3.c

@@ -0,0 +1,7 @@
+// Examples of failed array initialization. 
+// See: https://github.com/rems-project/cerberus/issues/253
+
+int a[][1][1] = {{{8}}};
+
+int b[1][1] = {5, {a}};
+

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

@@ -0,0 +1,8 @@
+// Example of negating a long integer literal. Broken as of 2024-7-4. 
+// See: https://github.com/rems-project/cerberus/issues/257
+
+// Type error: 
+void long_type_err_1() { 
+ -1l; 
+ return; 
+}

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

@@ -0,0 +1,11 @@
+// Bug: throws a type error
+// Derived from src/example-archive/c-testsuite/broken/error-proof/00038.err1.c
+// See https://github.com/rems-project/cerberus/issues/272
+
+int
+main()
+{
+ int size1 = sizeof(int); // <- works 
+ size1 = size1 + 1; // <- also works 
+ int size2 = sizeof(int) + 1; // <- fails 
+}

src/example-archive/simple-examples/working/int_to_char_1.c

@@ -0,0 +1,14 @@
+// Take an integer and require that it is small enough to represent as a char.
+// Then safely store the result in a char variable. Without the requires clause
+// this would be UB 
+
+void 
+int_to_char_1(int a) 
+/*@ requires 
+ (i32) MINu8() <= (i32) a; 
+ (i32) a <= (i32) MAXu8(); @*/
+{
+ char b; 
+ b = a; 
+ return; 
+}

src/example-archive/simple-examples/working/lemma_1.c

@@ -0,0 +1,13 @@
+// An example of defining and applying a trivial lemma 
+
+/*@
+ lemma lem_trivial ()
+ requires true;
+ ensures true; 
+@*/
+
+void lemma_1() 
+{
+ /*@ apply lem_trivial(); @*/
+ ; 
+}

src/example-archive/simple-examples/working/pred_2.c

@@ -0,0 +1,79 @@
+// Examples encoding control-flow for predicates. These are a contrived to work
+// around a CN parser issue. See https://github.com/rems-project/cerberus/issues/266 
+
+// Variant 1 - this works: 
+/*@ 
+predicate (i32) TestMemoryEqZero_2_var1(pointer p) {
+ take PVal = Owned<int>(p); 
+ let rval = test_if_zero(PVal); 
+ return rval; 
+}
+
+function (i32) test_if_zero(i32 x) {
+ if (x == 0i32) {
+ 1i32
+ } else { 
+ 0i32 
+ }
+}
+@*/
+
+void pred_2_var1(int *p) 
+/*@ requires 
+ take PreP = Owned<int>(p); 
+ PreP == 0i32; @*/
+/*@ ensures 
+ take TestP = TestMemoryEqZero_2_var1(p); 
+ TestP == 1i32; @*/
+{ 
+ ; 
+}
+
+// Variant 2 - this works: 
+/*@ 
+predicate (i32) TestMemoryEqZero_2_var2(pointer p) {
+ take PVal = Owned<int>(p); 
+ take rval = TestMemoryEqZero_2_Helper(p, PVal); 
+ return rval; 
+}
+
+predicate (i32) TestMemoryEqZero_2_Helper(pointer p, i32 x) {
+ if (x == 0i32) {
+ return 1i32; 
+ } else { 
+ return 0i32; 
+ }
+}
+@*/
+
+void pred_2_var2(int *p) 
+/*@ requires 
+ take PreP = Owned<int>(p); 
+ PreP == 0i32; @*/
+/*@ ensures 
+ take TestP = TestMemoryEqZero_2_var2(p); 
+ TestP == 1i32; @*/
+{ 
+ ; 
+}
+
+// Variant 3 - this works: 
+/*@ 
+predicate (i32) TestMemoryEqZero_2_var3(pointer p) {
+ take PVal = Owned<int>(p); 
+ let rval = (PVal == 0i32 ? 1i32 : 0i32); 
+ return rval; 
+}
+@*/
+
+void pred_2_var3(int *p) 
+/*@ requires 
+ take PreP = Owned<int>(p); 
+ PreP == 0i32; @*/
+/*@ ensures 
+ take TestP = TestMemoryEqZero_2_var3(p); 
+ TestP == 1i32; @*/
+{ 
+ ; 
+}
+