fix flattening of ID_invalid_pointer

Author: kroening

regression/cbmc/memory_allocation1/test.desc

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

src/analyses/goto_check.cpp

@@ -1003,8 +1003,7 @@ void goto_checkt::pointer_validity_check(
         guard);
     }
 
-    if(flags.is_unknown() ||
-       flags.is_integer_address())
+    if(flags.is_unknown())
       add_guarded_claim(
         or_exprt(allocs, not_exprt(invalid_pointer(pointer))),
         "dereference failure: pointer invalid",
@@ -1023,8 +1022,7 @@ void goto_checkt::pointer_validity_check(
         guard);
 
     if(flags.is_unknown() ||
-       flags.is_dynamic_heap() ||
-       flags.is_integer_address())
+       flags.is_dynamic_heap())
       add_guarded_claim(
         or_exprt(allocs, not_exprt(deallocated(pointer, ns))),
         "dereference failure: deallocated dynamic object",
@@ -1034,8 +1032,7 @@ void goto_checkt::pointer_validity_check(
         guard);
 
     if(flags.is_unknown() ||
-       flags.is_dynamic_local() ||
-       flags.is_integer_address())
+       flags.is_dynamic_local())
       add_guarded_claim(
         or_exprt(allocs, not_exprt(dead_object(pointer, ns))),
         "dereference failure: dead object",
@@ -1045,8 +1042,7 @@ void goto_checkt::pointer_validity_check(
         guard);
 
     if(flags.is_unknown() ||
-       flags.is_dynamic_heap() ||
-       flags.is_integer_address())
+       flags.is_dynamic_heap())
     {
       const or_exprt dynamic_bounds(
         dynamic_object_lower_bound(pointer, ns, access_lb),
@@ -1067,8 +1063,7 @@ void goto_checkt::pointer_validity_check(
 
     if(flags.is_unknown() ||
        flags.is_dynamic_local() ||
-       flags.is_static_lifetime() ||
-       flags.is_integer_address())
+       flags.is_static_lifetime())
     {
       const or_exprt object_bounds(
         object_lower_bound(pointer, ns, access_lb),
@@ -1082,6 +1077,18 @@ void goto_checkt::pointer_validity_check(
         expr,
         guard);
     }
+
+    if(flags.is_unknown() ||
+       flags.is_integer_address())
+    {
+      add_guarded_claim(
+        implies_exprt(integer_address(pointer), allocs),
+        "dereference failure: invalid integer address",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
+    }
   }
 }
 

src/solvers/flattening/bv_pointers.cpp

@@ -29,26 +29,19 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
 
       if(!bv.empty())
       {
-        bvt invalid_bv, null_bv;
+        bvt invalid_bv;
         encode(pointer_logic.get_invalid_object(), invalid_bv);
-        encode(pointer_logic.get_null_object(),    null_bv);
 
-        bvt equal_invalid_bv, equal_null_bv;
+        bvt equal_invalid_bv;
         equal_invalid_bv.resize(object_bits);
-        equal_null_bv.resize(object_bits);
 
         for(std::size_t i=0; i<object_bits; i++)
         {
           equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
                                           invalid_bv[offset_bits+i]);
-          equal_null_bv[i]   =prop.lequal(bv[offset_bits+i],
-                                          null_bv[offset_bits+i]);
         }
 
-        literalt equal_invalid=prop.land(equal_invalid_bv);
-        literalt equal_null=prop.land(equal_null_bv);
-
-        return prop.lor(equal_invalid, equal_null);
+        return prop.land(equal_invalid_bv);
       }
     }
   }