@@ -77,9 +77,13 @@ bool is_ptr_comparison(const exprt &expr)
77
77
(expr.operands ()[1 ].type ().id () == ID_pointer);
78
78
}
79
79
80
- static bool is_access_expr (const irep_idt &id )
80
+ static bool is_access_expr (const exprt &expr )
81
81
{
82
- return id == ID_member || id == ID_index || id == ID_dereference;
82
+ if (auto tc = expr_try_dynamic_cast<typecast_exprt>(expr))
83
+ return is_access_expr (tc->op ());
84
+
85
+ return expr.id () == ID_member || expr.id () == ID_index ||
86
+ expr.id () == ID_dereference;
83
87
}
84
88
85
89
static bool is_object_creation (const irep_idt &id)
@@ -107,7 +111,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
107
111
return resolve_symbol (simplified_expr, ns);
108
112
109
113
if (
110
- is_access_expr (simplified_id ) || is_ptr_diff (simplified_expr) ||
114
+ is_access_expr (simplified_expr ) || is_ptr_diff (simplified_expr) ||
111
115
is_ptr_comparison (simplified_expr))
112
116
{
113
117
auto const operands = eval_operands (simplified_expr, *this , ns);
@@ -168,7 +172,9 @@ bool abstract_environmentt::assign(
168
172
std::stack<exprt> stactions; // I'm not a continuation, honest guv'
169
173
while (s.id () != ID_symbol)
170
174
{
171
- if (s.id () == ID_index || s.id () == ID_member || s.id () == ID_dereference)
175
+ if (
176
+ s.id () == ID_index || s.id () == ID_member || s.id () == ID_dereference ||
177
+ s.id () == ID_typecast)
172
178
{
173
179
stactions.push (s);
174
180
s = s.operands ()[0 ];
@@ -248,8 +254,8 @@ abstract_object_pointert abstract_environmentt::write(
248
254
const irep_idt &stack_head_id = next_expr.id ();
249
255
INVARIANT (
250
256
stack_head_id == ID_index || stack_head_id == ID_member ||
251
- stack_head_id == ID_dereference,
252
- " Write stack expressions must be index, member, or dereference " );
257
+ stack_head_id == ID_dereference || stack_head_id == ID_typecast ,
258
+ " Write stack expressions must be index, member, dereference, or typecast " );
253
259
254
260
return lhs->write (*this , ns, remaining_stack, next_expr, rhs, merge_write);
255
261
}
0 commit comments