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-primitives/exists_memory_checks/invalid_index_range.desc

@@ -4,7 +4,7 @@ invalid_index_range.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: SUCCESS
+^\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: UNKNOWN$
 line 9 dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
 --
 --

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -4,8 +4,8 @@ smt_missing_range_check.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS
-\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
+^\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: UNKNOWN$
+^\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE$
 --
 --
 Check that memory checks fail for pointer dereferences inside an existential

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

@@ -3,13 +3,13 @@ test_malloc_less_than_bound.c
 --no-malloc-may-fail --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
-\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
-\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+^\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: UNKNOWN$
+^\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE$
+^\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: UNKNOWN$
 ^VERIFICATION FAILED$
 --
 --

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);