Skip to content

Commit 8cd443c

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 3b17634 commit 8cd443c

File tree

1 file changed

+8
-2
lines changed

1 file changed

+8
-2
lines changed

src/goto-symex/field_sensitivity.cpp

+8-2
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,10 @@ exprt field_sensitivityt::get_fields(
133133
tmp.remove_level_2();
134134
tmp.set_expression(member);
135135
if(was_l2)
136-
result.add_to_operands(state.rename(tmp, ns).get());
136+
{
137+
result.add_to_operands(
138+
state.rename(get_fields(ns, state, tmp), ns).get());
139+
}
137140
else
138141
result.add_to_operands(get_fields(ns, state, tmp));
139142
}
@@ -162,7 +165,10 @@ exprt field_sensitivityt::get_fields(
162165
tmp.remove_level_2();
163166
tmp.set_expression(index);
164167
if(was_l2)
165-
result.add_to_operands(state.rename(tmp, ns).get());
168+
{
169+
result.add_to_operands(
170+
state.rename(get_fields(ns, state, tmp), ns).get());
171+
}
166172
else
167173
result.add_to_operands(get_fields(ns, state, tmp));
168174
}

0 commit comments

Comments
 (0)