Reorder address checks

This is a slight change in functionality. A future refactor of the
address checks will necessitate reordering these anyway, and doing it in
isolation first gives us some additional confidence that our refactor
didn’t have any unintended consequences aside from the reordering.

Also changes the regression tests that break because of the reorder.

Author: hannes-steffenhagen-diffblue

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

@@ -8,8 +8,8 @@ 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 invalid in \*s: FAILURE$
-^\[main.pointer_dereference.7\] .* dereference failure: pointer NULL in \*s: FAILURE$
+^\[main.pointer_dereference.6\] .* dereference failure: pointer NULL in \*s: FAILURE$
+^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid 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$

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 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.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.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

src/analyses/goto_check.cpp

@@ -1298,12 +1298,6 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
 
     const bool unknown = flags.is_unknown() || flags.is_uninitialized();
 
-    if(unknown)
-    {
-      conditions.push_back(conditiont{
-        not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
-    }
-
     if(unknown || flags.is_null())
     {
       conditions.push_back(conditiont(
@@ -1313,6 +1307,12 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         "pointer NULL"));
     }
 
+    if(unknown)
+    {
+      conditions.push_back(conditiont{
+        not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
+    }
+
     if(unknown || flags.is_dynamic_heap())
     {
       conditions.push_back(conditiont(