@@ -94,30 +94,30 @@ exprt field_sensitivityt::apply(
94
94
ssa_exprt tmp = to_ssa_expr (index.array ());
95
95
auto l2_index = state.rename (index.index (), ns);
96
96
l2_index.simplify (ns);
97
- auto l2_array = state.rename (index.array (), ns);
97
+ exprt l2_size = state.rename (
98
+ to_array_type (index.array ().type ()).size (), ns).get ();
98
99
bool was_l2 = !tmp.get_level_2 ().empty ();
99
100
100
- exprt array_size_expr = to_array_type (l2_array.get ().type ()).size ();
101
- if (array_size_expr.is_nil () && index.array ().id () == ID_symbol)
101
+ if (l2_size.is_nil () && index.array ().id () == ID_symbol)
102
102
{
103
103
// In case the array type was incomplete, attempt to retrieve it from
104
104
// the symbol table.
105
105
const symbolt *array_from_symbol_table = ns.get_symbol_table ()
106
106
.lookup (to_symbol_expr (index.array ()).get_identifier ());
107
107
if (array_from_symbol_table != nullptr )
108
- array_size_expr = to_array_type (array_from_symbol_table->type ).size ();
108
+ l2_size = to_array_type (array_from_symbol_table->type ).size ();
109
109
}
110
110
111
111
if (
112
- array_size_expr .id () == ID_constant &&
113
- numeric_cast_v<mp_integer>(to_constant_expr (array_size_expr ))
112
+ l2_size .id () == ID_constant &&
113
+ numeric_cast_v<mp_integer>(to_constant_expr (l2_size ))
114
114
<= max_field_sensitive_array_size )
115
115
{
116
116
if (l2_index.get ().id () == ID_constant)
117
117
{
118
118
// place the entire index expression, not just the array operand, in an
119
119
// SSA expression
120
- ssa_exprt ssa_array = to_ssa_expr (l2_array. get ());
120
+ ssa_exprt ssa_array = to_ssa_expr (index. array ());
121
121
ssa_array.remove_level_2 ();
122
122
index.array () = ssa_array.get_original_expr ();
123
123
index.index () = l2_index.get ();
@@ -131,7 +131,7 @@ exprt field_sensitivityt::apply(
131
131
{
132
132
// Expand the array and return `{array[0]; array[1]; ...}[index]`
133
133
exprt expanded_array =
134
- get_fields (ns, state, to_ssa_expr (l2_array. get ()));
134
+ get_fields (ns, state, to_ssa_expr (index. array ()));
135
135
return index_exprt{std::move (expanded_array), l2_index.get ()};
136
136
}
137
137
}
0 commit comments