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 @@ -3529,18 +3529,6 @@ class member_exprt:public unary_exprt
3529
3529
{
3530
3530
return op0 ();
3531
3531
}
3532
-
3533
- // Retrieves the object(symbol) this member corresponds to
3534
- inline const symbol_exprt &symbol () const
3535
- {
3536
- const exprt &op=op0 ();
3537
- if (op.id ()==ID_member)
3538
- {
3539
- return static_cast <const member_exprt &>(op).symbol ();
3540
- }
3541
-
3542
- return to_symbol_expr (op);
3543
- }
3544
3532
};
3545
3533
3546
3534
// / \brief Cast an exprt to a \ref member_exprt
You can’t perform that action at this time.
0 commit comments