@@ -229,32 +229,41 @@ static void clinit_wrapper_do_recursive_calls(
229
229
object_factory_parameterst parameters = object_factory_parameters;
230
230
parameters.function_id = clinit_wrapper_name (class_name);
231
231
232
- for (const auto &symbol : symbol_table.symbols )
232
+ std::vector<irep_idt> nondet_ids;
233
+ std::for_each (
234
+ symbol_table.symbols .begin (),
235
+ symbol_table.symbols .end (),
236
+ [&](const std::pair<irep_idt, symbolt> &symbol) {
237
+ if (
238
+ symbol.second .type .get (ID_C_class) == class_name &&
239
+ symbol.second .is_static_lifetime &&
240
+ !symbol.second .type .get_bool (ID_C_constant))
241
+ {
242
+ nondet_ids.push_back (symbol.first );
243
+ }
244
+ });
245
+
246
+ for (const auto &id : nondet_ids)
233
247
{
234
- if (
235
- symbol.second .type .get (ID_C_class) == class_name &&
236
- symbol.second .is_static_lifetime &&
237
- !symbol.second .type .get_bool (ID_C_constant))
238
- {
239
- const symbol_exprt new_global_symbol = symbol.second .symbol_expr ();
240
-
241
- parameters.max_nonnull_tree_depth =
242
- is_non_null_library_global (symbol.first )
243
- ? std::max (
244
- size_t (1 ), object_factory_parameters.max_nonnull_tree_depth )
245
- : object_factory_parameters.max_nonnull_tree_depth ;
246
-
247
- gen_nondet_init (
248
- new_global_symbol,
249
- init_body,
250
- symbol_table,
251
- source_locationt (),
252
- false ,
253
- allocation_typet::DYNAMIC,
254
- parameters,
255
- pointer_type_selector,
256
- update_in_placet::NO_UPDATE_IN_PLACE);
257
- }
248
+ const symbol_exprt new_global_symbol =
249
+ symbol_table.lookup_ref (id).symbol_expr ();
250
+
251
+ parameters.max_nonnull_tree_depth =
252
+ is_non_null_library_global (id)
253
+ ? std::max (
254
+ size_t (1 ), object_factory_parameters.max_nonnull_tree_depth )
255
+ : object_factory_parameters.max_nonnull_tree_depth ;
256
+
257
+ gen_nondet_init (
258
+ new_global_symbol,
259
+ init_body,
260
+ symbol_table,
261
+ source_locationt (),
262
+ false ,
263
+ allocation_typet::DYNAMIC,
264
+ parameters,
265
+ pointer_type_selector,
266
+ update_in_placet::NO_UPDATE_IN_PLACE);
258
267
}
259
268
}
260
269
}
0 commit comments