File tree 2 files changed +3
-15
lines changed
jbmc/unit/java-testing-utils
2 files changed +3
-15
lines changed Original file line number Diff line number Diff line change @@ -99,7 +99,7 @@ require_goto_statements::find_struct_component_assignments(
99
99
100
100
if (
101
101
superclass_expr.get_component_name () == supercomponent_name &&
102
- superclass_expr.symbol ( ).get_identifier () == structure_name)
102
+ to_symbol_expr ( superclass_expr.compound () ).get_identifier () == structure_name)
103
103
{
104
104
if (
105
105
code_assign.rhs () ==
@@ -121,8 +121,8 @@ require_goto_statements::find_struct_component_assignments(
121
121
// - component name: \p component_name
122
122
// - operand (component of): symbol for \p structure_name
123
123
if (
124
- member_expr.op ().id () == ID_symbol &&
125
- member_expr.symbol ( ).get_identifier () == structure_name &&
124
+ member_expr.compound ().id () == ID_symbol &&
125
+ to_symbol_expr ( member_expr.compound () ).get_identifier () == structure_name &&
126
126
member_expr.get_component_name () == component_name)
127
127
{
128
128
if (
Original file line number Diff line number Diff line change @@ -3918,18 +3918,6 @@ class member_exprt:public unary_exprt
3918
3918
{
3919
3919
return op0 ();
3920
3920
}
3921
-
3922
- // Retrieves the object(symbol) this member corresponds to
3923
- inline const symbol_exprt &symbol () const
3924
- {
3925
- const exprt &op=op0 ();
3926
- if (op.id ()==ID_member)
3927
- {
3928
- return static_cast <const member_exprt &>(op).symbol ();
3929
- }
3930
-
3931
- return to_symbol_expr (op);
3932
- }
3933
3921
};
3934
3922
3935
3923
/* ! \brief Cast a generic exprt to a \ref member_exprt
You can’t perform that action at this time.
0 commit comments