Fixed secondary issues arising from local_bitvector_analysis fix.

In particular, goto_check did not properly handle pointers whose value was an
integer address (such as int *p = 0x10 in the test case memory_allocation1).

This commit adds in pointer checks on pointers which are integer addresses,
treating them essentially the same as pointers which are unknown (and could
therefore point to any of the more well-defined types of memory objects),
except that they are known not to be null, so no check for NULL is needed.

Author: klaas

regression/cbmc/memory_allocation1/main.c

@@ -9,6 +9,8 @@ int main()
   assert(*p==42);
   *(p+1)=42;
   assert(*(p+1)==42);
+  *(p - 0x10) = 42;
+  assert(*(p - 0x10) == 42);
 
   return 0;
 }

regression/cbmc/memory_allocation1/test.desc

@@ -3,10 +3,10 @@ main.c
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[main.pointer_dereference.2\] dereference failure: pointer invalid in \*p: SUCCESS
+\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*p: SUCCESS
 \[main.assertion.1\] assertion \*p==42: SUCCESS
-\[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
+\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
 \[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
-\*\* 12 of 26 failed
+^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -991,7 +991,8 @@ void goto_checkt::pointer_validity_check(
       allocs=disjunction(disjuncts);
     }
 
-    if(flags.is_unknown() || flags.is_null())
+    if(flags.is_unknown() ||
+       flags.is_null())
     {
       add_guarded_claim(
         or_exprt(allocs, not_exprt(null_pointer(pointer))),
@@ -1002,7 +1003,8 @@ void goto_checkt::pointer_validity_check(
         guard);
     }
 
-    if(flags.is_unknown())
+    if(flags.is_unknown() ||
+       flags.is_integer_address())
       add_guarded_claim(
         or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
         "dereference failure: pointer invalid",
@@ -1020,7 +1022,9 @@ void goto_checkt::pointer_validity_check(
         expr,
         guard);
 
-    if(flags.is_unknown() || flags.is_dynamic_heap())
+    if(flags.is_unknown() ||
+       flags.is_dynamic_heap() ||
+       flags.is_integer_address())
       add_guarded_claim(
         or_exprt(allocs, not_exprt(deallocated(pointer, ns))),
         "dereference failure: deallocated dynamic object",
@@ -1029,7 +1033,9 @@ void goto_checkt::pointer_validity_check(
         expr,
         guard);
 
-    if(flags.is_unknown() || flags.is_dynamic_local())
+    if(flags.is_unknown() ||
+       flags.is_dynamic_local() ||
+       flags.is_integer_address())
       add_guarded_claim(
         or_exprt(allocs, not_exprt(dead_object(pointer, ns))),
         "dereference failure: dead object",
@@ -1038,7 +1044,9 @@ void goto_checkt::pointer_validity_check(
         expr,
         guard);
 
-    if(flags.is_unknown() || flags.is_dynamic_heap())
+    if(flags.is_unknown() ||
+       flags.is_dynamic_heap() ||
+       flags.is_integer_address())
     {
       const or_exprt dynamic_bounds(
         dynamic_object_lower_bound(pointer, ns, access_lb),
@@ -1059,7 +1067,8 @@ void goto_checkt::pointer_validity_check(
 
     if(flags.is_unknown() ||
        flags.is_dynamic_local() ||
-       flags.is_static_lifetime())
+       flags.is_static_lifetime() ||
+       flags.is_integer_address())
     {
       const or_exprt object_bounds(
         object_lower_bound(pointer, ns, access_lb),