Merge pull request #2626 from qaphla/local_bitvector_analysis_fix

Fixed a bug in local_bitvector_analysis wherein an expression's ID was used in place of the expression's type's ID.

Author: kroening

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),

src/analyses/local_bitvector_analysis.cpp

@@ -62,7 +62,7 @@ bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
 {
   localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier);
   if(it==locals.locals_map.end() ||
-     it->second.id()!=ID_pointer ||
+     it->second.type().id()!=ID_pointer ||
      dirty(identifier))
     return false;