cprover
Loading...
Searching...
No Matches
memory_snapshot_harness_generator.cpp
Go to the documentation of this file.
1/******************************************************************\
2
3Module: Harness to initialise memory from memory snapshot
4
5Author: Daniel Poetzl
6
7\******************************************************************/
8
9#include <algorithm>
10
13
15
16#include <json/json_parser.h>
17
19
20#include <util/arith_tools.h>
21#include <util/c_types.h>
23#include <util/fresh_symbol.h>
24#include <util/string2int.h>
25#include <util/string_utils.h>
26#include <util/symbol_table.h>
27
29 const std::string &option,
30 const std::list<std::string> &values)
31{
32 auto &require_exactly_one_value =
35 {
36 // the option belongs to recursive initialization
37 }
39 {
41 values.begin(), values.end());
42 }
44 {
45 for(auto const &array_size_pair : values)
46 {
47 try
48 {
49 std::string array;
50 std::string size;
51 split_string(array_size_pair, ':', array, size);
52 // --associated-array-size implies --treat-pointer-as-array
53 // but it is not an error to specify both, so we don't check
54 // for duplicates here
56 array);
57 auto const inserted =
60 if(!inserted.second)
61 {
63 "can not have two associated array sizes for one array",
65 }
66 }
67 catch(const deserialization_exceptiont &)
68 {
70 "'" + array_size_pair +
71 "' is in an invalid format for array size pair",
73 "array_name:size_name, where both are the names of global "
74 "variables"};
75 }
76 }
77 }
79 {
80 memory_snapshot_file = require_exactly_one_value(option, values);
81 }
83 {
84 initial_goto_location_line = require_exactly_one_value(option, values);
85 }
87 {
88 std::vector<std::string> havoc_candidates =
89 split_string(values.front(), ',', true);
90 for(const auto &candidate : havoc_candidates)
91 {
92 variables_to_havoc.insert(candidate);
93 }
94 }
96 {
97 initial_source_location_line = require_exactly_one_value(option, values);
98 }
99 else
100 {
102 "unrecognized option for memory snapshot harness generator",
103 "--" + option);
104 }
105}
106
108 const goto_modelt &goto_model)
109{
110 if(memory_snapshot_file.empty())
111 {
113 "option --memory_snapshot is required",
114 "--harness-type initialise-from-memory-snapshot");
115 }
116
118 {
120 "choose either source or goto location to specify the entry point",
121 "--initial-source/goto-location");
122 }
123
125 {
128 goto_model.goto_functions);
129 }
130 else
131 {
134 goto_model.goto_functions);
135 }
136
137 const symbol_tablet &symbol_table = goto_model.symbol_table;
138
139 const symbolt *called_function_symbol =
140 symbol_table.lookup(entry_location.function_name);
141
142 if(called_function_symbol == nullptr)
143 {
145 "function `" + id2string(entry_location.function_name) +
146 "` not found in the symbol table",
147 "--initial-location");
148 }
149}
150
152 const symbol_exprt &func_init_done_var,
153 goto_modelt &goto_model) const
154{
155 goto_functionst &goto_functions = goto_model.goto_functions;
156
157 goto_functiont &goto_function =
159
160 goto_programt &goto_program = goto_function.body;
161
162 const goto_programt::const_targett start_it =
163 goto_program.instructions.begin();
164
165 auto ins_it1 = goto_program.insert_before(
166 start_it,
167 goto_programt::make_goto(goto_program.const_cast_target(start_it)));
168 ins_it1->guard = func_init_done_var;
169
170 auto ins_it2 = goto_program.insert_after(
171 ins_it1,
173 code_assignt(func_init_done_var, true_exprt())));
174
175 goto_program.compute_location_numbers();
176 goto_program.insert_after(
177 ins_it2,
180}
181
183 const symbolt &snapshot_symbol,
184 symbol_tablet &symbol_table) const
185{
186 symbolt &tmp_symbol = get_fresh_aux_symbol(
187 snapshot_symbol.type,
188 "", // no prefix name
189 id2string(snapshot_symbol.base_name),
190 snapshot_symbol.location,
191 snapshot_symbol.mode,
192 symbol_table);
193 tmp_symbol.is_static_lifetime = true;
194 tmp_symbol.value = snapshot_symbol.value;
195
196 return tmp_symbol;
197}
198
200{
201 if(t.id() != ID_pointer)
202 return 0;
203 else
204 return pointer_depth(t.subtype()) + 1;
205}
206
208 const symbol_tablet &snapshot,
209 goto_modelt &goto_model) const
210{
211 recursive_initializationt recursive_initialization{
213
214 std::vector<std::pair<irep_idt, symbolt>> ordered_snapshot_symbols;
215 // sort the snapshot symbols so that the non-pointer symbols are first, then
216 // pointers, then pointers-to-pointers, etc. so that we don't assign
217 // uninitialized values
218 {
219 std::vector<std::pair<irep_idt, symbolt>> selected_snapshot_symbols;
220 using relationt = typename preordert<irep_idt>::relationt;
221 relationt reference_relation;
222
223 for(const auto &snapshot_pair : snapshot)
224 {
225 const auto name = id2string(snapshot_pair.first);
226 if(name.find(CPROVER_PREFIX) != 0)
227 {
229 snapshot_pair.second.value,
230 [&reference_relation, &snapshot_pair](const irep_idt &id) {
231 reference_relation.insert(std::make_pair(snapshot_pair.first, id));
232 });
233 selected_snapshot_symbols.push_back(snapshot_pair);
234 }
235 }
236 preordert<irep_idt> reference_order{reference_relation};
237 reference_order.sort(selected_snapshot_symbols, ordered_snapshot_symbols);
238 }
239
240 code_blockt code{};
241
242 // add initialization for existing globals
243 for(const auto &pair : goto_model.symbol_table)
244 {
245 const auto &global_symbol = pair.second;
247 {
248 auto symeexr = global_symbol.symbol_expr();
249 if(symeexr.type() == global_symbol.value.type())
250 code.add(code_assignt{symeexr, global_symbol.value});
251 }
252 }
253
254 for(const auto &pair : ordered_snapshot_symbols)
255 {
256 const symbolt &snapshot_symbol = pair.second;
257 symbol_tablet &symbol_table = goto_model.symbol_table;
258
259 auto should_get_fresh = [&symbol_table](const symbolt &symbol) {
260 return symbol_table.lookup(symbol.base_name) == nullptr &&
261 !symbol.is_type;
262 };
263 const symbolt &fresh_or_snapshot_symbol =
264 should_get_fresh(snapshot_symbol)
265 ? fresh_symbol_copy(snapshot_symbol, symbol_table)
266 : snapshot_symbol;
267
269 fresh_or_snapshot_symbol))
270 continue;
271
272 if(variables_to_havoc.count(fresh_or_snapshot_symbol.base_name) == 0)
273 {
274 code.add(code_assignt{fresh_or_snapshot_symbol.symbol_expr(),
275 fresh_or_snapshot_symbol.value});
276 }
277 else
278 {
279 recursive_initialization.initialize(
280 fresh_or_snapshot_symbol.symbol_expr(),
282 code);
283 }
284 }
285 return code;
286}
287
289 const symbolt &called_function_symbol,
290 code_blockt &code) const
291{
292 const code_typet &code_type = to_code_type(called_function_symbol.type);
293
295
296 for(const code_typet::parametert &parameter : code_type.parameters())
297 {
298 arguments.push_back(side_effect_expr_nondett{
299 parameter.type(), called_function_symbol.location});
300 }
301
302 code.add(code_function_callt{called_function_symbol.symbol_expr(),
303 std::move(arguments)});
304}
305
308 goto_modelt &goto_model,
309 const symbolt &function) const
310{
311 const auto r = goto_model.symbol_table.insert(function);
312 CHECK_RETURN(r.second);
313
314 auto function_iterator_pair = goto_model.goto_functions.function_map.emplace(
315 function.name, goto_functiont{});
316
317 CHECK_RETURN(function_iterator_pair.second);
318
319 goto_functiont &harness_function = function_iterator_pair.first->second;
320
322 goto_model.symbol_table, goto_model.goto_functions, message_handler);
323 harness_function.body.add(goto_programt::make_end_function());
324}
325
327 const std::string &file,
328 symbol_tablet &snapshot) const
329{
330 jsont json;
331
333
334 if(r)
335 {
336 throw deserialization_exceptiont("failed to read JSON memory snapshot");
337 }
338
339 if(json.is_array())
340 {
341 // since memory-analyzer produces an array JSON we need to search it
342 // to find the first JSON object that is a symbol table
343 const auto &jarr = to_json_array(json);
344 for(auto const &arr_element : jarr)
345 {
346 if(!arr_element.is_object())
347 continue;
348 const auto &json_obj = to_json_object(arr_element);
349 const auto it = json_obj.find("symbolTable");
350 if(it != json_obj.end())
351 {
352 symbol_table_from_json(json_obj, snapshot);
353 return;
354 }
355 }
357 "JSON memory snapshot does not contain symbol table");
358 }
359 else
360 {
361 // throws a deserialization_exceptiont or an
362 // incorrect_goto_program_exceptiont
363 // on failure to read JSON symbol table
364 symbol_table_from_json(json, snapshot);
365 }
366}
367
369 goto_modelt &goto_model,
370 const irep_idt &harness_function_name)
371{
372 symbol_tablet snapshot;
374
375 symbol_tablet &symbol_table = goto_model.symbol_table;
376 goto_functionst &goto_functions = goto_model.goto_functions;
377
378 const symbolt *called_function_symbol =
379 symbol_table.lookup(entry_location.function_name);
380 recursive_initialization_config.mode = called_function_symbol->mode;
381
382 // introduce a symbol for a Boolean variable to indicate the point at which
383 // the function initialisation is completed
384 auto &func_init_done_symbol = get_fresh_aux_symbol(
385 bool_typet(),
387 "func_init_done",
389 called_function_symbol->mode,
390 symbol_table);
391 func_init_done_symbol.is_static_lifetime = true;
392 func_init_done_symbol.value = false_exprt();
393 symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr();
394
395 add_init_section(func_init_done_var, goto_model);
396
397 code_blockt harness_function_body =
398 add_assignments_to_globals(snapshot, goto_model);
399
400 harness_function_body.add(code_assignt{func_init_done_var, false_exprt{}});
401
403 *called_function_symbol, harness_function_body);
404
405 // Create harness function symbol
406
407 symbolt harness_function_symbol;
408 harness_function_symbol.name = harness_function_name;
409 harness_function_symbol.base_name = harness_function_name;
410 harness_function_symbol.pretty_name = harness_function_name;
411
412 harness_function_symbol.is_lvalue = true;
413 harness_function_symbol.mode = called_function_symbol->mode;
414 harness_function_symbol.type = code_typet({}, empty_typet());
415 harness_function_symbol.value = harness_function_body;
416
417 // Add harness function to goto model and symbol table
418 insert_harness_function_into_goto_model(goto_model, harness_function_symbol);
419
420 goto_functions.update();
421}
422
425 const std::string &cmdl_option)
426{
427 std::vector<std::string> start = split_string(cmdl_option, ':', true);
428
429 if(
430 start.empty() || start.front().empty() ||
431 (start.size() == 2 && start.back().empty()) || start.size() > 2)
432 {
434 "invalid initial location specification", "--initial-location");
435 }
436
437 if(start.size() == 2)
438 {
439 const auto location_number = string2optional_unsigned(start.back());
440 CHECK_RETURN(location_number.has_value());
441 return entry_goto_locationt{start.front(), *location_number};
442 }
443 else
444 {
445 return entry_goto_locationt{start.front()};
446 }
447}
448
451 const std::string &cmdl_option)
452{
453 std::string initial_file_string;
454 std::string initial_line_string;
456 cmdl_option, ':', initial_file_string, initial_line_string, true);
457
458 if(initial_file_string.empty() || initial_line_string.empty())
459 {
461 "invalid initial location specification", "--initial-file-line");
462 }
463
464 const auto line_number = string2optional_unsigned(initial_line_string);
465 CHECK_RETURN(line_number.has_value());
466 return entry_source_locationt{initial_file_string, *line_number};
467}
468
471 const entry_goto_locationt &entry_goto_location,
472 const goto_functionst &goto_functions)
473{
474 PRECONDITION(!entry_goto_location.function_name.empty());
475 const irep_idt &function_name = entry_goto_location.function_name;
476
477 // by function(+location): search for the function then jump to n-th
478 // location, then check the number
479 const auto &goto_function =
480 goto_functions.function_map.find(entry_goto_location.function_name);
481 if(
482 goto_function != goto_functions.function_map.end() &&
483 goto_function->second.body_available())
484 {
485 const auto &goto_program = goto_function->second.body;
486
487 const auto corresponding_instruction =
488 entry_goto_location.find_first_corresponding_instruction(
489 goto_program.instructions);
490
491 if(corresponding_instruction != goto_program.instructions.end())
492 return entry_locationt{function_name, corresponding_instruction};
493 }
495 "could not find the specified entry point", "--initial-goto-location");
496}
497
500 const entry_source_locationt &entry_source_location,
501 const goto_functionst &goto_functions)
502{
503 PRECONDITION(!entry_source_location.file_name.empty());
504
505 source_location_matcht best_match;
506 // by line: iterate over all instructions until source location match
507 for(const auto &entry : goto_functions.function_map)
508 {
509 const auto &goto_function = entry.second;
510 // if !body_available() then body.instruction.empty() and that's fine
511 const auto &goto_program = goto_function.body;
512
513 const auto candidate_instruction =
514 entry_source_location.find_first_corresponding_instruction(
515 goto_program.instructions);
516
517 if(candidate_instruction.first != goto_program.instructions.end())
518 {
519 best_match.match_up(
520 candidate_instruction.second, entry.first, candidate_instruction.first);
521 }
522 }
523
524 if(best_match.match_found)
525 return entry_locationt{best_match.function_name, best_match.instruction};
526 else
528 "could not find the specified entry point", "--initial-source-location");
529}
530
533 const goto_programt::instructionst &instructions) const
534{
535 if(!location_number.has_value())
536 return instructions.begin();
537
538 return std::find_if(
539 instructions.begin(),
540 instructions.end(),
541 [this](const goto_programt::instructiont &instruction) {
542 return *location_number == instruction.location_number;
543 });
544}
545
546std::pair<goto_programt::const_targett, size_t>
549 const goto_programt::instructionst &instructions) const
550{
551 auto it = std::find_if(
552 instructions.begin(),
553 instructions.end(),
554 [this](const goto_programt::instructiont &instruction) {
555 return instruction.source_location().get_file() == file_name &&
556 safe_string2unsigned(id2string(
557 instruction.source_location().get_line())) >= line_number;
558 });
559
560 if(it == instructions.end())
561 return {it, 0};
562 else
563 return {it,
564 safe_string2unsigned(id2string(it->source_location().get_line())) -
566}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
unsignedbv_typet size_type()
Definition: c_types.cpp:68
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
codet representation of a function call statement.
exprt::operandst argumentst
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
The empty type.
Definition: std_types.h:51
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
A collection of goto functions.
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition: goto_program.h:602
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
instructionst::const_iterator const_targett
Definition: goto_program.h:593
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< instructiont > instructionst
Definition: goto_program.h:590
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:755
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & id() const
Definition: irep.h:396
Definition: json.h:27
void add_init_section(const symbol_exprt &func_init_done_var, goto_modelt &goto_model) const
Modify the entry-point function to start from the user-specified initial location.
entry_locationt entry_location
data to initialize the entry function
void insert_harness_function_into_goto_model(goto_modelt &goto_model, const symbolt &function) const
Insert the function into the symbol table (and the goto functions map) of the goto_model.
entry_locationt initialize_entry_via_goto(const entry_goto_locationt &entry_goto_location, const goto_functionst &goto_functions)
Find and return the entry instruction (requested by the user as goto location: function name + locati...
entry_source_locationt parse_source_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry source location.
entry_locationt initialize_entry_via_source(const entry_source_locationt &entry_source_location, const goto_functionst &goto_functions)
Find and return the entry instruction (requested by the user as source location: file name + line num...
void handle_option(const std::string &option, const std::list< std::string > &values) override
Collect the memory-snapshot specific cmdline options (one at a time)
void get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const
Parse the snapshot JSON file and initialise the symbol table.
entry_goto_locationt parse_goto_location(const std::string &cmdl_option)
Parse a command line option to extract the user specified entry goto location.
void collect_references(const exprt &expr, Adder &&add_reference) const
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
The main function of this harness, consists of the following:
void add_call_with_nondet_arguments(const symbolt &called_function_symbol, code_blockt &code) const
Create as many non-deterministic arguments as there are arguments of the called_function_symbol and a...
recursive_initialization_configt recursive_initialization_config
void validate_options(const goto_modelt &goto_model) override
Check that user options make sense: On their own, e.g.
const symbolt & fresh_symbol_copy(const symbolt &snapshot_symbol, symbol_tablet &symbol_table) const
Introduce a new symbol into symbol_table with the same name and type as snapshot_symbol.
std::string memory_snapshot_file
data to store the command-line options
code_blockt add_assignments_to_globals(const symbol_tablet &snapshot, goto_modelt &goto_model) const
For each global symbol in the snapshot symbol table either: 1) add code_assignt assigning a value fro...
size_t pointer_depth(const typet &t) const
Recursively compute the pointer depth.
Class for generating initialisation code for compound structures.
static bool is_initialization_allowed(const symbolt &symbol)
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
static const source_locationt & nil()
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
#define CPROVER_PREFIX
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static int8_t r
Definition: irep_hash.h:60
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table)
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT
#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT
#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT
#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT
#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT
std::string require_exactly_one_value(const std::string &option, const std::list< std::string > &values)
Returns the only value of a single element list, throws an exception if not passed a single element l...
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
optionalt< unsigned > string2optional_unsigned(const std::string &str, int base)
Convert string to unsigned similar to the stoul or stoull functions, return nullopt when the conversi...
Definition: string2int.cpp:64
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:16
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: kdev_t.h:19
User provided goto location: function name and (maybe) location number; the structure wraps this opti...
goto_programt::const_targett find_first_corresponding_instruction(const goto_programt::instructionst &instructions) const
Returns the first goto_programt::instructiont represented by this goto location, i....
Wraps the information needed to identify the entry point.
User provided source location: file name and line number; the structure wraps this option with a pars...
std::pair< goto_programt::const_targett, size_t > find_first_corresponding_instruction(const goto_programt::instructionst &instructions) const
Returns the first goto_programt::instructiont represented by this source location,...
void sort(const std::vector< std::pair< Key, T > > &input, std::vector< std::pair< Key, T > > &output)
Wraps the information for source location match candidates.
void match_up(const size_t &candidate_distance, const irep_idt &candidate_function_name, const goto_programt::const_targett &candidate_instruction)
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
std::set< irep_idt > pointers_to_treat_as_arrays
Author: Diffblue Ltd.