pointer checks are now fatal

The checks for

* pointer dereferences
* pointer relations
* pointer arithmetic

are designed to identify cases of undefined behavior.  They must be fatal.

Author: kroening

regression/cbmc/Function_Pointer18/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
 \[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS

regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function foo
+--function foo --no-pointer-check
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 4: SUCCESS$
 ^EXIT=10$

regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function foo
+--function foo --no-pointer-check
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) >= 4: SUCCESS$
 ^EXIT=10$

regression/cbmc/array-cell-sensitivity10/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 16.*SUCCESS$
 ^\[main.assertion\.2\] line 17.*FAILURE$

regression/cbmc/array-cell-sensitivity3/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 9.*SUCCESS$
 ^\[main.assertion\.2\] line 10.*FAILURE$

regression/cbmc/array-cell-sensitivity7/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 10.*SUCCESS$
 ^\[main.assertion\.2\] line 11.*FAILURE$

regression/cbmc/array-cell-sensitivity8/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 11.*SUCCESS$
 ^\[main.assertion\.2\] line 12.*FAILURE$

regression/cbmc/byte_update14/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 10.*SUCCESS$
 ^\[main.assertion\.2\] line 11.*FAILURE$

regression/cbmc/memory_allocation1/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$
 ^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$
 ^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$
-^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: SUCCESS$
+^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: UNKNOWN$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/pointer-extra-checks/main.c

@@ -1,28 +1,33 @@
+int nondet_int();
+
 int main()
 {
+  int i = nondet_int();
+
+  if(i == 0)
   {
     int *p = 0x0;
 
     // Since local_bitvector_analysis can tell that p is NULL, this should
     // generate only a NULL check, and not any of the other pointer checks.
     *p = 1;
   }
-
+  else if(i == 1)
   {
     int i;
     int *q = &i;
 
     // This should only generate a not-dead check and a bounds-check.
     *q = 2;
   }
-
+  else if(i == 2)
   {
     int *r = __CPROVER_allocate(sizeof(int), 1);
 
     // This should generate a not-deallocated check and a bounds-check.
     *r = 5;
   }
-
+  else if(i == 3)
   {
     int *s;
 

regression/cbmc/ptr_arithmetic_on_null/test.desc

@@ -1,6 +1,6 @@
 CORE gcc-only
 main.c
-
+--no-pointer-check
 ^\[main.assertion.1\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ (\(.*\))?1: SUCCESS$
 ^\[main.assertion.2\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 - (\(.*\))?1: SUCCESS$
 ^\[main.assertion.3\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ \(.*\)offset: SUCCESS$

regression/cbmc/switch8/test.desc

@@ -8,7 +8,7 @@ main.c
 ^\[main\.pointer_dereference\.1\] line 36 dereference failure: dead object in \*p: SUCCESS$
 ^\[main\.pointer_dereference\.2\] line 36 dereference failure: pointer outside object bounds in \*p: SUCCESS$
 ^\[main\.assertion\.3\] line 42 assertion \*p == 42: FAILURE$
-^\[main\.pointer_dereference\.5\] line 42 dereference failure: pointer outside object bounds in \*p: SUCCESS$
+^\[main\.pointer_dereference\.5\] line 42 dereference failure: pointer outside object bounds in \*p: UNKNOWN$
 ^\[main\.pointer_dereference\.3\] line 42 dereference failure: pointer NULL in \*p: SUCCESS$
 ^\[main\.pointer_dereference\.4\] line 42 dereference failure: dead object in \*p: FAILURE$
 ^\[main\.assertion\.4\] line 49 assertion e == 42: FAILURE$

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -1368,7 +1368,7 @@ void goto_check_ct::pointer_rel_check(
           c.assertion,
           "pointer relation: " + c.description,
           "pointer arithmetic",
-          false, // fatal
+          true, // fatal
           expr.find_source_location(),
           pointer,
           guard);
@@ -1427,7 +1427,7 @@ void goto_check_ct::pointer_overflow_check(
       c.assertion,
       "pointer arithmetic: " + c.description,
       "pointer arithmetic",
-      false, // fatal
+      true, // fatal
       expr.find_source_location(),
       expr,
       guard);
@@ -1469,7 +1469,7 @@ void goto_check_ct::pointer_validity_check(
       c.assertion,
       "dereference failure: " + c.description,
       "pointer dereference",
-      false, // fatal
+      true, // fatal
       src_expr.find_source_location(),
       src_expr,
       guard);