refactor pointer_validity_check using address_check

Author: Daniel Kroening

regression/cbmc/Function5/test.desc

@@ -3,6 +3,6 @@ main.c
 --pointer-check --bounds-check
 ^SIGNAL=0$
 ^EXIT=10$
-^\[.*\] dereference failure: pointer outside object bounds in \*p: FAILURE$
+^\[.*\] pointer outside object bounds in \*p: FAILURE$
 --
 ^warning: ignoring

regression/cbmc/address_space_size_limit3/test.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^.* dereference failure: pointer outside object bounds in .*: FAILURE$
+^.* pointer outside object bounds in .*: FAILURE$
 --
 ^warning: ignoring
 --

regression/cbmc/memory_allocation1/test.desc

@@ -3,9 +3,9 @@ main.c
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.pointer_dereference\.2\] dereference failure: invalid integer address in \*p: SUCCESS$
+^\[main\.pointer_dereference\.2\] 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\.pointer_dereference\.[0-9]+\] invalid integer address in p\[.*1\]: FAILURE$
 ^\[main\.assertion\.2\] assertion \*\(p\+1\)==42: SUCCESS$
 ^VERIFICATION FAILED$
 --

regression/cbmc/pointer-extra-checks/test.desc

@@ -3,37 +3,37 @@ main.c
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.pointer_dereference.1\] dereference failure: pointer NULL in \*p: FAILURE$
-^\[main.pointer_dereference.2\] dereference failure: dead object in \*q: SUCCESS$
-^\[main.pointer_dereference.3\] dereference failure: pointer outside object bounds in \*q: SUCCESS$
-^\[main.pointer_dereference.4\] dereference failure: deallocated dynamic object in \*r: SUCCESS$
-^\[main.pointer_dereference.5\] dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
-^\[main.pointer_dereference.6\] dereference failure: pointer uninitialized in \*s: FAILURE$
+^\[main.pointer_dereference.1\] pointer NULL in \*p: FAILURE$
+^\[main.pointer_dereference.2\] dead object in \*q: SUCCESS$
+^\[main.pointer_dereference.3\] pointer outside object bounds in \*q: SUCCESS$
+^\[main.pointer_dereference.4\] deallocated dynamic object in \*r: SUCCESS$
+^\[main.pointer_dereference.5\] pointer outside dynamic object bounds in \*r: SUCCESS$
+^\[main.pointer_dereference.6\] pointer uninitialized in \*s: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*p:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*p:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*p:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*p:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*p:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*p:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*q:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*q:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*q:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*q:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*q:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*r:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*r:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*r:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*r:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*r:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*s:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*s:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*s:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*s:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*s:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*s:
+^\[main.pointer_dereference.[0-9]+\] pointer invalid in \*p:
+^\[main.pointer_dereference.[0-9]+\] pointer uninitialized in \*p:
+^\[main.pointer_dereference.[0-9]+\] deallocated dynamic object in \*p:
+^\[main.pointer_dereference.[0-9]+\] dead object in \*p:
+^\[main.pointer_dereference.[0-9]+\] pointer outside dynamic object bounds in \*p:
+^\[main.pointer_dereference.[0-9]+\] pointer outside object bounds in \*p:
+^\[main.pointer_dereference.[0-9]+\] pointer NULL in \*q:
+^\[main.pointer_dereference.[0-9]+\] pointer invalid in \*q:
+^\[main.pointer_dereference.[0-9]+\] deallocated dynamic object in \*q:
+^\[main.pointer_dereference.[0-9]+\] pointer outside dynamic object bounds in \*q:
+^\[main.pointer_dereference.[0-9]+\] pointer uninitialized in \*q:
+^\[main.pointer_dereference.[0-9]+\] pointer NULL in \*r:
+^\[main.pointer_dereference.[0-9]+\] pointer invalid in \*r:
+^\[main.pointer_dereference.[0-9]+\] pointer uninitialized in \*r:
+^\[main.pointer_dereference.[0-9]+\] dead object in \*r:
+^\[main.pointer_dereference.[0-9]+\] pointer outside object bounds in \*r:
+^\[main.pointer_dereference.[0-9]+\] pointer NULL in \*s:
+^\[main.pointer_dereference.[0-9]+\] pointer invalid in \*s:
+^\[main.pointer_dereference.[0-9]+\] deallocated dynamic object in \*s:
+^\[main.pointer_dereference.[0-9]+\] dead object in \*s:
+^\[main.pointer_dereference.[0-9]+\] pointer outside dynamic object bounds in \*s:
+^\[main.pointer_dereference.[0-9]+\] pointer outside object bounds in \*s:
 --
 This test ensures that local_bitvector_analysis is correctly labelling obvious
 cases of pointers and that --pointer-check is not generating excess assertions.

regression/cbmc/read1/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[.*] dereference failure: pointer outside object bounds in .*: FAILURE
+\[.*] pointer outside object bounds in .*: FAILURE
 \*\* 1 of .* failed \(.*\)
 --
 ^warning: ignoring