@@ -172,75 +172,6 @@ void local_value_sett::make_union_adjusting_types(
172
172
}
173
173
}
174
174
175
- // / Builds a version of expr suitable for alias-comparison
176
- // / \param expr: The expression to be converted to the alias-uniform structure
177
- // / \return expr without information which is irrelevant to alias-comparison
178
- static exprt get_uniform_expr (const exprt &expr)
179
- {
180
- if (const auto desc_ptr = expr_try_dynamic_cast<object_descriptor_exprt>(expr))
181
- {
182
- object_descriptor_exprt ob;
183
- ob.object () = get_uniform_expr (desc_ptr->object ());
184
- ob.offset () = desc_ptr->offset ();
185
- return ob;
186
- }
187
- if (can_cast_expr<external_value_set_exprt>(expr))
188
- {
189
- exprt copy = expr;
190
- copy.set (ID_is_initializer, ID_0);
191
- return copy;
192
- }
193
- return expr;
194
- }
195
-
196
- // / Reconstructs a type of a pointer to the object expr
197
- // / \param expr: An object in a points-to set we make an alias type for
198
- // / \return A type of a pointer to the object expr
199
- static typet get_alias_type (const exprt &expr)
200
- {
201
- if (expr.id () == ID_object_descriptor)
202
- {
203
- object_descriptor_exprt ob_expr = to_object_descriptor_expr (expr);
204
- if (
205
- ob_expr.offset ().id () == ID_invalid ||
206
- ob_expr.offset ().id () == ID_unknown)
207
- {
208
- return pointer_type (ob_expr.object ().type ());
209
- }
210
- }
211
- return pointer_type (expr.type ());
212
- }
213
-
214
- void local_value_sett::get_may_alias_set (
215
- const exprt &expr,
216
- value_setst::valuest &dest,
217
- const namespacet &ns) const
218
- {
219
- TMPROF_BLOCK ();
220
-
221
- object_mapt pointed_objects;
222
- get_value_set (expr, pointed_objects, ns, false );
223
- std::vector<exprt> uniform_pointed_objects;
224
- for (const auto &num_obj : pointed_objects.read ())
225
- uniform_pointed_objects.push_back (get_uniform_expr (to_expr (num_obj)));
226
-
227
- for (const auto &name_entry : values)
228
- for (const auto &enum_eobj : name_entry.second .object_map .read ())
229
- {
230
- if (
231
- std::find (
232
- uniform_pointed_objects.cbegin (),
233
- uniform_pointed_objects.cend (),
234
- get_uniform_expr (to_expr (enum_eobj))) !=
235
- uniform_pointed_objects.cend ())
236
- {
237
- dest.push_back (
238
- symbol_exprt (
239
- name_entry.second .identifier , get_alias_type (to_expr (enum_eobj))));
240
- }
241
- }
242
- }
243
-
244
175
// / Value-set analysis accrues a `suffix` as it walks down an expression tree--
245
176
// / for example, it transforms a `get_value_set_rec(x.y.z)` into
246
177
// / `get_value_set_rec(x, suffix = ".y.z")`. This function recovers the type
0 commit comments