Skip to content

Commit

Permalink
Field sensitivity: also rewrite byte extract to type casts
Browse files Browse the repository at this point in the history
With model-checking/kani#2456 we see examples
where a pointer of a different type is byte-extracted from a union. This
is caused by Rust's niche placement. `get_subexpression_at_offset`
already catered for that, but we didn't use it in field expansion.
  • Loading branch information
tautschnig committed May 30, 2023
1 parent d5e13f1 commit a939baf
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions src/goto-symex/field_sensitivity.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,20 @@ exprt field_sensitivityt::apply(
else
return apply(ns, state, std::move(tmp), write);
}
else if(
recursive_member.has_value() && recursive_member->id() == ID_typecast)
{
if(was_l2)
{
return apply(
ns,
state,
state.rename(std::move(*recursive_member), ns).get(),
write);
}
else
return apply(ns, state, std::move(*recursive_member), write);
}
}
}
}
Expand Down

0 comments on commit a939baf

Please sign in to comment.