Add regression tests to for inconsistent assumptions involving __CPROVER_r_ok()

Adds tests to check that inconsistent assumptions involving __CPROVER_r_ok() can
be detected by checking if a subsequent assert(0) fails.

Author: danpoe

regression/cbmc/r_w_ok_inconsistent_dead/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p;
+
+  {
+    char c;
+    p = &c;
+  }
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_dead/test-no-cp.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--function test_global_pointer --pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to an out of scope
+variable and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_dead/test.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--function test_global_pointer --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to an out of scope
+variable and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_deallocated/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  free(p);
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_deallocated/test-no-cp.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc/r_w_ok_inconsistent_deallocated/test.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc/r_w_ok_inconsistent_integer/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void test_global_pointer()
+{
+  char *p = (size_t)123 << (sizeof(char *) * 8 - 1) | 123;
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails without constant propagator
+  *p; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_integer/test-no-cp.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc/r_w_ok_inconsistent_integer/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer initialized to an
+integer address not pointing to memory and __CPROVER_r_ok() can be detected via
+assert(0).

regression/cbmc/r_w_ok_inconsistent_invalid/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  // special value of invalid pointer
+  char *p = (size_t)1 << (sizeof(char *) * 8 - 8);
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails
+  *p; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_invalid/test-no-cp.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving the special invalid pointer
+value and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_invalid/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving the special invalid pointer
+value and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_nondet/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+void main()
+{
+  char *p = nondet(); 
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails
+  *p; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_nondet/test-no-cp.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a nondet pointer and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_nondet/test.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a nondet pointer and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_null/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = NULL;
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // succeeds
+  *p; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_null/test-no-cp.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a null pointer and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_null/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a null pointer and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_valid/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char c1;
+
+void main()
+{
+  char c2;
+
+  char *p1 = &c1;
+  char *p2 = &c2;
+  char *p3 = malloc(1);
+
+  __CPROVER_assume(
+    __CPROVER_r_ok(p1, 2) ||
+    __CPROVER_r_ok(p1 - 1, 1) ||
+    __CPROVER_r_ok(p1 + 1, 1) ||
+    __CPROVER_r_ok(p2, 2) ||
+    __CPROVER_r_ok(p2 - 1, 1) ||
+    __CPROVER_r_ok(p2 + 1, 1) ||
+    __CPROVER_r_ok(p3, 2) ||
+    __CPROVER_r_ok(p3 - 1, 1) ||
+    __CPROVER_r_ok(p3 + 1, 1));
+  
+  assert(0); // succeeds
+  *p1; // succeeds
+  *p2; // succeeds
+  *p3; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_valid/test-no-cp.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to a valid memory
+object (though potentially with an offset that is out of bounds) and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_valid/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to a valid memory
+object (though potentially with an offset that is out of bounds) and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_valid_negated/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char c1;
+
+void main()
+{
+  char c2;
+
+  char *p1 = &c1;
+  char *p2 = &c2;
+
+  char *p3 = malloc(1);
+  __CPROVER_assume(p1 != NULL);
+  
+  __CPROVER_assume(
+    !__CPROVER_r_ok(p1, 1) ||
+    !__CPROVER_r_ok(p2, 1) ||
+    !__CPROVER_r_ok(p3, 1));
+
+  assert(0);
+  *p1;
+  *p2;
+  *p3;
+}

regression/cbmc/r_w_ok_inconsistent_valid_negated/test-no-cp.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a valid pointer and a negated
+use of __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_valid_negated/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a valid pointer and a negated
+use of __CPROVER_r_ok() can be detected via assert(0).