Skip to content

Commit 1d2a052

Browse files
committed
Revert "integer dereferences are now re-written to a custom expression"
This reverts commit 2b17564. ID_integer_dereference has not been supported in any back-end. The new pointer encoding should happily take care of such integer -> pointer type casts.
1 parent a7e4c18 commit 1d2a052

File tree

2 files changed

+7
-5
lines changed

2 files changed

+7
-5
lines changed

src/pointer-analysis/dereference.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -265,17 +265,20 @@ exprt dereferencet::dereference_typecast(
265265
return dereference_rec(op, offset, type); // just pass down
266266
else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
267267
{
268-
// We got an integer-typed address A. We turn this
269-
// into integer_dereference(A+offset),
270-
// and then let some other layer worry about it.
268+
// We got an integer-typed address A. We turn this back (!)
269+
// into *(type *)(A+offset), and then let some other layer
270+
// worry about it.
271271

272272
exprt integer=op;
273273

274274
if(!offset.is_zero())
275275
integer=
276276
plus_exprt(offset, typecast_exprt(op, offset.type()));
277277

278-
return unary_exprt(ID_integer_dereference, integer, type);
278+
exprt new_typecast=
279+
typecast_exprt(integer, pointer_type(type));
280+
281+
return dereference_exprt(new_typecast, type);
279282
}
280283
else
281284
throw "dereferencet: unexpected cast";

src/util/irep_ids.def

-1
Original file line numberDiff line numberDiff line change
@@ -826,7 +826,6 @@ IREP_ID_ONE(array_replace)
826826
IREP_ID_ONE(switch_case_number)
827827
IREP_ID_ONE(java_array_access)
828828
IREP_ID_ONE(java_member_access)
829-
IREP_ID_ONE(integer_dereference)
830829
IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter)
831830
IREP_ID_TWO(C_java_generic_type, #java_generic_type)
832831
IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)

0 commit comments

Comments
 (0)