Skip to content

Commit 348b4f7

Browse files
Field sensitivity applies to constant size arrays
The array size must be constant for field sensitivity to apply.
1 parent 13ad887 commit 348b4f7

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/goto-symex/field_sensitivity.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@ exprt field_sensitivityt::apply(
9191
index.array().id() == ID_symbol &&
9292
index.array().get_bool(ID_C_SSA_symbol) &&
9393
index.array().type().id() == ID_array &&
94+
to_array_type(index.array().type()).size().id() == ID_constant &&
9495
index.index().id() == ID_constant)
9596
{
9697
// place the entire index expression, not just the array operand, in an

0 commit comments

Comments
 (0)