Add __CPROVER_is_invalid_pointer regression test

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/pointers/pointer_is_invalid.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  // special value of the invalid pointer (object bits = 1 and offset = 0), as
+  // checked for by __CPROVER_is_invalid_pointer()
+  char *p = (size_t)1 << (sizeof(char *) * 8 - 8);
+  __CPROVER_assert(
+    __CPROVER_is_invalid_pointer(p), "INVALID pointer, so passing");
+  int i;
+  __CPROVER_assert(
+    __CPROVER_is_invalid_pointer(&i), "VALID pointer, so failing");
+}

regression/cbmc-incr-smt2/pointers/pointer_is_invalid.desc

@@ -0,0 +1,13 @@
+CORE
+pointer_is_invalid.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ INVALID pointer, so passing: SUCCESS
+\[main\.assertion\.2\] line \d+ VALID pointer, so failing: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Tests that an inconsistent assumption involving the special invalid pointer
+value and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-incr-smt2/pointers/pointer_object3.c

@@ -12,8 +12,9 @@ int main()
     __CPROVER_POINTER_OBJECT(NULL) != 0,
     "expected to fail with object ID == 0");
   // In the case where the program contains a single address of operation,
-  // the pointer object is going to be 1.
+  // the pointer object is going to be 2 (1 is invalid pointer that is tested
+  // somewhere else).
   __CPROVER_assert(
-    __CPROVER_POINTER_OBJECT(&foo) != 1,
-    "expected to fail with object ID == 1");
+    __CPROVER_POINTER_OBJECT(&foo) != 2,
+    "expected to fail with object ID == 2");
 }

regression/cbmc-incr-smt2/pointers/pointer_object3.desc

@@ -2,7 +2,7 @@ CORE
 pointer_object3.c
 
 \[main\.assertion\.1] line \d+ expected to fail with object ID == 0: FAILURE
-\[main\.assertion\.2] line \d+ expected to fail with object ID == 1: FAILURE
+\[main\.assertion\.2] line \d+ expected to fail with object ID == 2: FAILURE
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$