Make pointer-primitive-check a no-op when behaviour is always defined

doc/architectural/memory-primitives.md

@@ -199,17 +199,21 @@ CBMC has the option `--pointer-primitive-check` to detect potential misuses of
 the memory primitives. It checks that the pointers that appear in the following
 primitives are either null or valid:
 
-- `__CPROVER_POINTER_OBJECT`
-- `__CPROVER_POINTER_OFFSET`
-- `__CPROVER_same_object`
 - `__CPROVER_OBJECT_SIZE`
 - `__CPROVER_DYNAMIC_OBJECT`
 - `__CPROVER_r_ok`
 - `__CPROVER_w_ok`
 
-While the first three primitives have well-defined semantics even on invalid
-pointers, using them on invalid pointers is usually unintended in user programs.
-Thus, they have been included in the `--pointer-primitive-check` option.
+The following three primitives have well-defined semantics even on invalid
+pointers. Thus, they have been excluded from the `--pointer-primitive-check`
+option.
+
+- `__CPROVER_POINTER_OBJECT`
+- `__CPROVER_POINTER_OFFSET`
+- `__CPROVER_same_object`
+
+Using them on invalid pointers, however, may still be unintended in user
+programs.
 
 <sup>1</sup> Pointers with negative offsets never point to memory objects.
 Negative values are used internally to detect pointer underflows.

regression/cbmc/pointer-primitive-check-01/test.desc

@@ -3,35 +3,36 @@ main.c
 --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[main.pointer_primitives.1\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
-\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
-\[main.pointer_primitives.3\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
-\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
-\[main.pointer_primitives.5\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
-\[main.pointer_primitives.6\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
-\[main.pointer_primitives.7\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
-\[main.pointer_primitives.8\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
-\[main.pointer_primitives.9\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
-\[main.pointer_primitives.10\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
-\[main.pointer_primitives.11\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
-\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
-\[main.pointer_primitives.13\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
-\[main.pointer_primitives.14\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
-\[main.pointer_primitives.15\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
-\[main.pointer_primitives.16\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
-\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
-\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
-\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
-\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
-\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
-\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
-\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
-\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
-\[main.pointer_primitives.25\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
-\[main.pointer_primitives.26\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
-\[main.pointer_primitives.27\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
-\[main.pointer_primitives.28\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
 --
 ^warning: ignoring
+\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
+\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
+\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
+\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
+\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
+\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
+\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
+\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
+\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
+\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
+\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
+\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
 --
-Verifies that checks are added for all pointer primitives
+Verifies that checks are added for exactly those pointer primitives that are not
+universally well defined.

regression/cbmc/pointer-primitive-check-02/main.c

@@ -4,8 +4,8 @@ char *p1;
 
 void main()
 {
-  __CPROVER_POINTER_OBJECT(p1);
+  __CPROVER_r_ok(p1, 1);
 
   char *p2 = NULL;
-  __CPROVER_POINTER_OBJECT(p2);
+  __CPROVER_r_ok(p2, 1);
 }

regression/cbmc/pointer-primitive-check-03/main.c

@@ -4,37 +4,37 @@ void main()
 {
   // uninitialized pointer
   char *p1;
-  __CPROVER_POINTER_OBJECT(p1);
+  __CPROVER_r_ok(p1, 1);
 
   // special value of invalid pointer
   char *p2 = (size_t)1 << (sizeof(char *) * 8 - 8);
-  __CPROVER_POINTER_OBJECT(p2);
+  __CPROVER_r_ok(p2, 1);
 
   // pointer object 123, offset 123, not pointing to valid memory
   char *p3 = ((size_t)123 << (sizeof(char *) * 8 - 8)) | 123;
-  __CPROVER_POINTER_OBJECT(p3);
+  __CPROVER_r_ok(p3, 1);
 
   // negative offset
   char *p4 = malloc(1);
   p4 -= 1;
-  __CPROVER_POINTER_OBJECT(p4);
+  __CPROVER_r_ok(p4, 1);
 
   // offset out of bounds
   char *p5 = malloc(10);
   p5 += 10;
-  __CPROVER_POINTER_OBJECT(p5);
+  __CPROVER_r_ok(p5, 1);
 
   // dead
   char *p6;
   {
     char c;
     p6 = &c;
   }
-  __CPROVER_POINTER_OBJECT(p6);
+  __CPROVER_r_ok(p6, 1);
   *p6;
 
   // deallocated
   char *p7 = malloc(1);
   free(p7);
-  __CPROVER_POINTER_OBJECT(p7);
+  __CPROVER_r_ok(p7, 1);
 }

regression/cbmc/pointer-primitive-check-03/test.desc

@@ -3,45 +3,14 @@ main.c
 --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
+^\[main.pointer_primitives.\d+\] line 7 .* in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 11 .* in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 15 .* in R_OK\(p3, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 20 .* in R_OK\(p4, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 25 .* in R_OK\(p5, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 33 .* in R_OK\(p6, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 39 .* in R_OK\(p7, \(unsigned (long (long )?)?int\)1\): FAILURE$
 --
-\[main.pointer_primitives.1\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p1): SUCCESS
-\[main.pointer_primitives.2\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p1): FAILURE
-\[main.pointer_primitives.3\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p1): SUCCESS
-\[main.pointer_primitives.4\] line \d+ dead object in POINTER_OBJECT((const void \*)p1): SUCCESS
-\[main.pointer_primitives.5\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p1): FAILURE
-\[main.pointer_primitives.6\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p1): FAILURE
-\[main.pointer_primitives.7\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p2): SUCCESS
-\[main.pointer_primitives.8\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p2): FAILURE
-\[main.pointer_primitives.9\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p2): SUCCESS
-\[main.pointer_primitives.10\] line \d+ dead object in POINTER_OBJECT((const void \*)p2): SUCCESS
-\[main.pointer_primitives.11\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p2): SUCCESS
-\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p2): FAILURE
-\[main.pointer_primitives.13\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p3): SUCCESS
-\[main.pointer_primitives.14\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p3): SUCCESS
-\[main.pointer_primitives.15\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p3): SUCCESS
-\[main.pointer_primitives.16\] line \d+ dead object in POINTER_OBJECT((const void \*)p3): SUCCESS
-\[main.pointer_primitives.17\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p3): FAILURE
-\[main.pointer_primitives.18\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p3): FAILURE
-\[main.pointer_primitives.19\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p4): SUCCESS
-\[main.pointer_primitives.20\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p4): SUCCESS
-\[main.pointer_primitives.21\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p4): SUCCESS
-\[main.pointer_primitives.22\] line \d+ dead object in POINTER_OBJECT((const void \*)p4): SUCCESS
-\[main.pointer_primitives.23\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p4): FAILURE
-\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p4): SUCCESS
-\[main.pointer_primitives.25\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p5): SUCCESS
-\[main.pointer_primitives.26\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p5): SUCCESS
-\[main.pointer_primitives.27\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p5): SUCCESS
-\[main.pointer_primitives.28\] line \d+ dead object in POINTER_OBJECT((const void \*)p5): SUCCESS
-\[main.pointer_primitives.29\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p5): FAILURE
-\[main.pointer_primitives.30\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p5): SUCCESS
-\[main.pointer_primitives.31\] line \d+ dead object in POINTER_OBJECT((const void \*)p6): FAILURE
-\[main.pointer_primitives.32\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p6): SUCCESS
-\[main.pointer_primitives.33\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p7): SUCCESS
-\[main.pointer_primitives.34\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p7): SUCCESS
-\[main.pointer_primitives.35\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p7): FAILURE
-\[main.pointer_primitives.36\] line \d+ dead object in POINTER_OBJECT((const void \*)p7): SUCCESS
-\[main.pointer_primitives.37\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS
-\[main.pointer_primitives.38\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS
 ^warning: ignoring
 --
 Verifies that the pointer primitives check fails for the various forms of

regression/cbmc/pragma_cprover3/main.c

@@ -8,13 +8,19 @@ int main()
 #pragma CPROVER check push
 #pragma CPROVER check disable "pointer-primitive"
   // do not generate checks for the following statements
-  if(__CPROVER_same_object(p, q))
+  if(__CPROVER_r_ok(p, sizeof(*p) + 2))
   {
   }
 #pragma CPROVER check pop
 
-  // generate check and fail on the following statements
+  // no checks are generated for the following statement as the behaviour is
+  // always defined
   if(__CPROVER_same_object(p, q))
   {
   }
+
+  // generate check and fail on the following statements
+  if(__CPROVER_r_ok(q, 1))
+  {
+  }
 }

regression/cbmc/pragma_cprover3/test.desc

@@ -2,15 +2,12 @@ CORE
 main.c
 --pointer-primitive-check
 ^main.c function main$
-^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
-^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
+^\[main.pointer_primitives.\d+\] line 11
+^\[main.pointer_primitives.\d+\] line 18
+--

regression/cbmc/pragma_cprover_enable3/main.c

@@ -1,20 +1,17 @@
-#include <stdlib.h>
-
 int main()
 {
-  char *p = malloc(sizeof(*p));
-  char *q;
+  char *p, *q;
 
 #pragma CPROVER check push
 #pragma CPROVER check enable "pointer-primitive"
   // generate checks for the following statements and fail
-  if(__CPROVER_same_object(p, q))
+  if(__CPROVER_r_ok(p, 1))
   {
   }
 #pragma CPROVER check pop
 
   // but do not generate checks on the following statements
-  if(__CPROVER_same_object(p, q))
+  if(__CPROVER_r_ok(q, 1))
   {
   }
 }

regression/cbmc/pragma_cprover_enable3/test.desc

@@ -2,17 +2,11 @@ CORE
 main.c
 
 ^main.c function main$
-^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
-^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
-^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main.pointer_primitives.\d+\] line 17
+^\[main.pointer_primitives.\d+\] line 14
 --

regression/cbmc/pragma_cprover_enable_all/main.c

@@ -34,10 +34,10 @@ int main()
     float x;
     float y;
     ABC e;
-    bool same;
+    bool readable;
     char i;
     signed int j;
-    same = __CPROVER_same_object(p, q);
+    readable = __CPROVER_r_ok(q, 1);
     q = p + 2000000000000;
     q = r;
     if(nondet_bool())
@@ -71,10 +71,10 @@ int main()
     float x;
     float y;
     ABC e;
-    bool same;
+    bool readable;
     char i;
     signed int j;
-    same = __CPROVER_same_object(p, q);
+    readable = __CPROVER_r_ok(q, 1);
     q = p + 2000000000000;
     q = r;
     if(nondet_bool())

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -1,8 +1,8 @@
 CORE broken-smt-backend
 main.c
 --object-bits 8 --bounds-check --pointer-check --pointer-primitive-check --div-by-zero-check --enum-range-check --unsigned-overflow-check --signed-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --undefined-shift-check --nan-check --pointer-primitive-check
-^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE
-^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE
+^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE
 ^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE
 ^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
@@ -14,8 +14,8 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in POINTER_OBJECT\(const void \*\)q\): FAILURE
-^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in POINTER_OBJECT\(const void \*\)q\): FAILURE
+^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE
 ^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE
 ^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE
@@ -24,4 +24,4 @@ main.c
 ^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
 ^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE
 --
-This test uses all possible named-checks to maximize coverage.
+This test uses all possible named-checks to maximize coverage.