Merge pull request diffblue#1453 from diffblue/integer-addressees

integer dereferences are now re-written to a custom expression

Author: Daniel Kroening

src/pointer-analysis/dereference.cpp

@@ -264,20 +264,17 @@ exprt dereferencet::dereference_typecast(
     return dereference_rec(op, offset, type); // just pass down
   else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
   {
-    // We got an integer-typed address A. We turn this back (!)
-    // into *(type *)(A+offset), and then let some other layer
-    // worry about it.
+    // We got an integer-typed address A. We turn this
+    // into integer_dereference(A+offset),
+    // and then let some other layer worry about it.
 
     exprt integer=op;
 
     if(!offset.is_zero())
       integer=
         plus_exprt(offset, typecast_exprt(op, offset.type()));
 
-    exprt new_typecast=
-      typecast_exprt(integer, pointer_type(type));
-
-    return dereference_exprt(new_typecast, type);
+    return unary_exprt(ID_integer_dereference, integer, type);
   }
   else
     throw "dereferencet: unexpected cast";

src/util/irep_ids.def

@@ -823,6 +823,7 @@ IREP_ID_ONE(array_replace)
 IREP_ID_ONE(switch_case_number)
 IREP_ID_ONE(java_array_access)
 IREP_ID_ONE(java_member_access)
+IREP_ID_ONE(integer_dereference)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO