@@ -77,9 +77,13 @@ bool is_ptr_comparison(const exprt &expr)
7777 (expr.operands ()[1 ].type ().id () == ID_pointer);
7878}
7979
80- static bool is_access_expr (const irep_idt &id )
80+ static bool is_access_expr (const exprt &expr )
8181{
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;
8387}
8488
8589static bool is_object_creation (const irep_idt &id)
@@ -107,7 +111,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
107111 return resolve_symbol (simplified_expr, ns);
108112
109113 if (
110- is_access_expr (simplified_id ) || is_ptr_diff (simplified_expr) ||
114+ is_access_expr (simplified_expr ) || is_ptr_diff (simplified_expr) ||
111115 is_ptr_comparison (simplified_expr))
112116 {
113117 auto const operands = eval_operands (simplified_expr, *this , ns);
@@ -168,7 +172,9 @@ bool abstract_environmentt::assign(
168172 std::stack<exprt> stactions; // I'm not a continuation, honest guv'
169173 while (s.id () != ID_symbol)
170174 {
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)
172178 {
173179 stactions.push (s);
174180 s = s.operands ()[0 ];
@@ -248,8 +254,8 @@ abstract_object_pointert abstract_environmentt::write(
248254 const irep_idt &stack_head_id = next_expr.id ();
249255 INVARIANT (
250256 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 " );
253259
254260 return lhs->write (*this , ns, remaining_stack, next_expr, rhs, merge_write);
255261}
0 commit comments