Update existing regression tests for new updated address_check() implementation

Author: danpoe

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

@@ -8,7 +8,13 @@ main.c
 ^\[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.6\] .* dereference failure: pointer invalid in \*s: FAILURE$
+^\[main.pointer_dereference.7\] .* dereference failure: pointer NULL in \*s: FAILURE$
+^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
+^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
+^\[main.pointer_dereference.10\] .* dereference failure: pointer outside dynamic object bounds in \*s: FAILURE$
+^\[main.pointer_dereference.11\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
+^\[main.pointer_dereference.12\] .* dereference failure: invalid integer address in \*s: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
@@ -28,12 +34,6 @@ main.c
 ^\[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:
 --
 This test ensures that local_bitvector_analysis is correctly labelling obvious
 cases of pointers and that --pointer-check is not generating excess assertions.

regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

@@ -3,8 +3,8 @@ test.c
 --harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
 ^EXIT=0$
 ^SIGNAL=0$
-\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
-\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS