Adding pointer-primitive to the list of named checks that can be disabled using pragmas.

Author: Remi Delmas

doc/cprover-manual/properties.md

@@ -122,6 +122,7 @@ The goto-instrument program supports these checks:
 | `--bounds-check`             |  add array bounds checks                             |
 | `--div-by-zero-check`        |  add division by zero checks                         |
 | `--pointer-check`            |  add pointer checks                                  |
+| `--pointer-primitive-check`  |  add pointer primitive checks                        |
 | `--signed-overflow-check`    |  add arithmetic over- and underflow checks           |
 | `--unsigned-overflow-check`  |  add arithmetic over- and underflow checks           |
 | `--undefined-shift-check`    |  add range checks for shift distances                |

regression/cbmc/pragma_cprover3/main.c

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

regression/cbmc/pragma_cprover3/test.desc

@@ -0,0 +1,16 @@
+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$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--

src/ansi-c/scanner.l

@@ -234,9 +234,10 @@ CPROVER_PREFIX  "__CPROVER_"
 
 arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero")
 enum_check      "enum-range"
+pointer_primitive "pointer-primitive"
 memory_check    ("bounds"|"pointer"|"memory_leak")
 overflow_check  ("signed"|"unsigned"|"pointer"|"float")"-overflow"
-named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check})["]
+named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check}|{pointer_primitive})["]
 
 %x GRAMMAR
 %x COMMENT1