Skip to content

Commit 5b86aba

Browse files
smowtontautschnig
authored andcommitted
field_sensitivityt::get_fields: recurse on operands even when input is already L2
For an L1 or lower expression, get_fields already recursed, e.g. to turn `x` -> `{ { x..a..g, x..a..h }, x..b }` rather than `{ x..a, a..b }` when its `a` member is itself struct-typed. However this recursion was omitted in the case where the input expression is already L2 renamed.
1 parent 63936ad commit 5b86aba

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/goto-symex/field_sensitivity.cpp

+4-1
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,10 @@ exprt field_sensitivityt::get_fields(
128128
tmp.remove_level_2();
129129
tmp.set_expression(member);
130130
if(was_l2)
131-
result.add_to_operands(state.rename(tmp, ns).get());
131+
{
132+
result.add_to_operands(
133+
state.rename(get_fields(ns, state, tmp), ns).get());
134+
}
132135
else
133136
result.add_to_operands(get_fields(ns, state, tmp));
134137
}

0 commit comments

Comments
 (0)