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,30 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char *p;
+
+void test_global_pointer()
+{
+  {
+    char c;
+    p = &c;
+  }
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p; // succeeds
+}
+
+void test_local_pointer()
+{
+  char *q;
+
+  {
+    char c;
+    q = &c;
+  }
+
+  __CPROVER_assume(__CPROVER_r_ok(q, 1));
+  assert(0); // fails
+  *q; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_dead/test-global-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-global.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_dead/test-local-no-cp.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--function test_local_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-local.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--function test_local_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,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char *p;
+
+void test_global_pointer()
+{
+  p = malloc(1);
+  free(p);
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p; // succeeds
+}
+
+void test_local_pointer()
+{
+  char *q;
+
+  q = malloc(1);
+  free(q);
+
+  __CPROVER_assume(__CPROVER_r_ok(q, 1));
+  assert(0); // fails
+  *q; // succeeds
+}

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

@@ -0,0 +1,11 @@
+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 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-global.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--function test_global_pointer --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_deallocated/test-local-no-cp.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--function test_local_pointer --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-local.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--function test_local_pointer --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,22 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char *p;
+
+void test_global_pointer()
+{
+  p = (size_t)123 << (sizeof(char *) * 8 - 1) | 123;
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails without constant propagator
+  *p; // succeeds
+}
+
+void test_local_pointer()
+{
+  char *q;
+
+  q = (size_t)123 << (sizeof(char *) * 8 - 1) | 123;;
+  __CPROVER_assume(__CPROVER_r_ok(q, 10));
+  assert(0); // fails without constant propagator
+  *q; // succeeds
+}

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

@@ -0,0 +1,11 @@
+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 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-global.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--function test_global_pointer --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/test-local-no-cp.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--function test_local_pointer --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-local.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--function test_local_pointer --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,24 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char *p;
+
+void test_global_pointer()
+{
+  // special value of invalid pointer
+  p = (size_t)1 << (sizeof(char *) * 8 - 8);
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails
+  *p; // succeeds
+}
+
+void test_local_pointer()
+{
+  char *q;
+
+  // special value of invalid pointer
+  q = (size_t)1 << (sizeof(char *) * 8 - 8);
+  __CPROVER_assume(__CPROVER_r_ok(q, 10));
+  assert(0); // fails
+  *q; // succeeds
+}

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function test_global_pointer --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-global.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function test_global_pointer --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_invalid/test-local-no-cp.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function test_local_pointer --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-local.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function test_local_pointer --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,21 @@
+#include <assert.h>
+
+char *p;
+
+void test_global_pointer()
+{
+  p = nondet(); 
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // fails
+  *p; // succeeds
+}
+
+void test_local_pointer()
+{
+  char *q;
+
+  q = nondet(); 
+  __CPROVER_assume(__CPROVER_r_ok(q, 10));
+  assert(0); // fails
+  *q; // succeeds
+}

regression/cbmc/r_w_ok_inconsistent_nondet/test-global-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 nondet pointer and
+__CPROVER_r_ok() can be detected via assert(0).

regression/cbmc/r_w_ok_inconsistent_nondet/test-global.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 nondet pointer and
+__CPROVER_r_ok() can be detected via assert(0).

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

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--function test_local_pointer --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-local.desc

@@ -0,0 +1,10 @@
+FUTURE
+main.c
+--function test_local_pointer --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,22 @@
+#include <assert.h>
+#include <stdlib.h>
+
+char *p;
+
+void test_global_pointer()
+{
+  p = NULL;
+  __CPROVER_assume(__CPROVER_r_ok(p, 10));
+  assert(0); // succeeds
+  *p; // succeeds
+}
+
+void test_local_pointer()
+{
+  char *q;
+
+  q = NULL;
+  __CPROVER_assume(__CPROVER_r_ok(q, 10));
+  assert(0); // succeeds
+  *q; // succeeds
+}

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

@@ -0,0 +1,10 @@
+CORE
+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 null pointer and
+__CPROVER_r_ok() can be detected via assert(0).