cprover
generate_function_bodies.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Replace bodies of goto functions
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
12
17
18#include <util/format_expr.h>
19#include <util/fresh_symbol.h>
20#include <util/make_unique.h>
21#include <util/pointer_expr.h>
22#include <util/prefix.h>
23#include <util/string2int.h>
24#include <util/string_utils.h>
25
27 goto_functiont &function,
28 symbol_tablet &symbol_table,
29 const irep_idt &function_name) const
30{
31 PRECONDITION(!function.body_available());
32 generate_parameter_names(function, symbol_table, function_name);
33 generate_function_body_impl(function, symbol_table, function_name);
34}
35
37 goto_functiont &function,
38 symbol_tablet &symbol_table,
39 const irep_idt &function_name) const
40{
41 auto &function_symbol = symbol_table.get_writeable_ref(function_name);
42 auto &parameters = to_code_type(function_symbol.type).parameters();
43
44 int param_counter = 0;
45 for(auto &parameter : parameters)
46 {
47 if(parameter.get_identifier().empty())
48 {
49 const std::string param_base_name =
50 parameter.get_base_name().empty()
51 ? "__param$" + std::to_string(param_counter++)
52 : id2string(parameter.get_base_name());
53 irep_idt new_param_identifier =
54 id2string(function_name) + "::" + param_base_name;
55 parameter.set_base_name(param_base_name);
56 parameter.set_identifier(new_param_identifier);
57 parameter_symbolt new_param_sym;
58 new_param_sym.name = new_param_identifier;
59 new_param_sym.type = parameter.type();
60 new_param_sym.base_name = param_base_name;
61 new_param_sym.mode = function_symbol.mode;
62 new_param_sym.module = function_symbol.module;
63 new_param_sym.location = function_symbol.location;
64 symbol_table.add(new_param_sym);
65 }
66 }
67 function.set_parameter_identifiers(to_code_type(function_symbol.type));
68}
69
71{
72protected:
74 goto_functiont &function,
75 symbol_tablet &symbol_table,
76 const irep_idt &function_name) const override
77 {
78 auto const &function_symbol = symbol_table.lookup_ref(function_name);
79 // NOLINTNEXTLINE
80 auto add_instruction = [&](goto_programt::instructiont &&i) {
81 auto instruction = function.body.add(std::move(i));
82 instruction->source_location_nonconst() = function_symbol.location;
83 return instruction;
84 };
86 add_instruction(goto_programt::make_end_function());
87 }
88};
89
91{
92protected:
94 goto_functiont &function,
95 symbol_tablet &symbol_table,
96 const irep_idt &function_name) const override
97 {
98 auto const &function_symbol = symbol_table.lookup_ref(function_name);
99 // NOLINTNEXTLINE
100 auto add_instruction = [&](goto_programt::instructiont &&i) {
101 auto instruction = function.body.add(std::move(i));
102 instruction->source_location_nonconst() = function_symbol.location;
103 instruction->source_location_nonconst().set_function(function_name);
104 return instruction;
105 };
106 auto assert_instruction =
107 add_instruction(goto_programt::make_assertion(false_exprt()));
108 const namespacet ns(symbol_table);
109 std::ostringstream comment_stream;
110 comment_stream << id2string(ID_assertion) << " "
111 << format(assert_instruction->get_condition());
112 assert_instruction->source_location_nonconst().set_comment(
113 comment_stream.str());
114 assert_instruction->source_location_nonconst().set_property_class(
115 ID_assertion);
116 add_instruction(goto_programt::make_end_function());
117 }
118};
119
122{
123protected:
125 goto_functiont &function,
126 symbol_tablet &symbol_table,
127 const irep_idt &function_name) const override
128 {
129 auto const &function_symbol = symbol_table.lookup_ref(function_name);
130 // NOLINTNEXTLINE
131 auto add_instruction = [&](goto_programt::instructiont &&i) {
132 auto instruction = function.body.add(std::move(i));
133 instruction->source_location_nonconst() = function_symbol.location;
134 instruction->source_location_nonconst().set_function(function_name);
135 return instruction;
136 };
137 auto assert_instruction =
138 add_instruction(goto_programt::make_assertion(false_exprt()));
139 const namespacet ns(symbol_table);
140 std::ostringstream comment_stream;
141 comment_stream << id2string(ID_assertion) << " "
142 << format(assert_instruction->get_condition());
143 assert_instruction->source_location_nonconst().set_comment(
144 comment_stream.str());
145 assert_instruction->source_location_nonconst().set_property_class(
146 ID_assertion);
148 add_instruction(goto_programt::make_end_function());
149 }
150};
151
153{
154public:
156 std::vector<irep_idt> globals_to_havoc,
157 std::regex parameters_to_havoc,
159 message_handlert &message_handler)
164 message(message_handler)
165 {
166 }
167
169 std::vector<irep_idt> globals_to_havoc,
170 std::vector<std::size_t> param_numbers_to_havoc,
172 message_handlert &message_handler)
177 message(message_handler)
178 {
179 }
180
181private:
183 const exprt &lhs,
184 const std::size_t initial_depth,
185 const source_locationt &source_location,
186 const irep_idt &function_id,
187 symbol_tablet &symbol_table,
188 goto_programt &dest) const
189 {
190 symbol_factoryt symbol_factory(
191 symbol_table,
192 source_location,
193 function_id,
196
197 code_blockt assignments;
198
199 symbol_factory.gen_nondet_init(
200 assignments,
201 lhs,
202 initial_depth,
204 false); // do not initialize const objects at the top level
205
206 code_blockt init_code;
207
208 symbol_factory.declare_created_symbols(init_code);
209 init_code.append(assignments);
210
211 goto_programt tmp_dest;
213 init_code, symbol_table, tmp_dest, message.get_message_handler(), ID_C);
214
215 dest.destructive_append(tmp_dest);
216 }
217
219 const std::string &param_name,
220 std::size_t param_number) const
221 {
222 if(parameters_to_havoc.has_value())
223 {
224 return std::regex_match(param_name, *parameters_to_havoc);
225 }
226 else
227 {
229 return std::binary_search(
230 param_numbers_to_havoc->begin(),
232 param_number);
233 }
234 }
235
236protected:
238 goto_functiont &function,
239 symbol_tablet &symbol_table,
240 const irep_idt &function_name) const override
241 {
242 const namespacet ns(symbol_table);
243 // some user input checking
244 if(param_numbers_to_havoc.has_value() && !param_numbers_to_havoc->empty())
245 {
246 auto max_param_number = std::max_element(
248 if(*max_param_number >= function.parameter_identifiers.size())
249 {
251 "function " + id2string(function_name) + " does not take " +
252 std::to_string(*max_param_number + 1) + " arguments",
253 "--generate-havocing-body"};
254 }
255 for(const auto number : *param_numbers_to_havoc)
256 {
257 const auto &parameter = function.parameter_identifiers[number];
258 const symbolt &parameter_symbol = ns.lookup(parameter);
259 if(parameter_symbol.type.id() != ID_pointer)
260 {
262 "argument number " + std::to_string(number) + " of function " +
263 id2string(function_name) + " is not a pointer",
264 "--generate-havocing-body"};
265 }
266 }
267 }
268
269 auto const &function_symbol = symbol_table.lookup_ref(function_name);
270 // NOLINTNEXTLINE
271 auto add_instruction = [&](goto_programt::instructiont &&i) {
272 auto instruction = function.body.add(std::move(i));
273 instruction->source_location_nonconst() = function_symbol.location;
274 return instruction;
275 };
276
277 for(std::size_t i = 0; i < function.parameter_identifiers.size(); ++i)
278 {
279 const auto &parameter = function.parameter_identifiers[i];
280 const symbolt &parameter_symbol = ns.lookup(parameter);
281 if(
282 parameter_symbol.type.id() == ID_pointer &&
283 !to_pointer_type(parameter_symbol.type)
284 .base_type()
285 .get_bool(ID_C_constant) &&
286 should_havoc_param(id2string(parameter_symbol.base_name), i))
287 {
288 auto goto_instruction =
290 parameter_symbol.symbol_expr(),
291 null_pointer_exprt(to_pointer_type(parameter_symbol.type)))));
292
293 dereference_exprt dereference_expr(
294 parameter_symbol.symbol_expr(),
295 to_pointer_type(parameter_symbol.type).base_type());
296
297 goto_programt dest;
299 dereference_expr,
300 1, // depth 1 since we pass the dereferenced pointer
301 function_symbol.location,
302 function_name,
303 symbol_table,
304 dest);
305
306 function.body.destructive_append(dest);
307
308 auto label_instruction = add_instruction(goto_programt::make_skip());
309 goto_instruction->complete_goto(label_instruction);
310 }
311 }
312
313 for(auto const &global_id : globals_to_havoc)
314 {
315 auto const &global_sym = symbol_table.lookup_ref(global_id);
316
317 goto_programt dest;
318
320 symbol_exprt(global_sym.name, global_sym.type),
321 0,
322 function_symbol.location,
323 irep_idt(),
324 symbol_table,
325 dest);
326
327 function.body.destructive_append(dest);
328 }
329
330 const typet &return_type = to_code_type(function_symbol.type).return_type();
331 if(return_type != empty_typet())
332 {
333 typet type(return_type);
334 type.remove(ID_C_constant);
335
336 symbolt &aux_symbol = get_fresh_aux_symbol(
337 type,
338 id2string(function_name),
339 "return_value",
340 function_symbol.location,
341 ID_C,
342 symbol_table);
343
344 aux_symbol.is_static_lifetime = false;
345
346 add_instruction(goto_programt::make_decl(aux_symbol.symbol_expr()));
347
348 goto_programt dest;
349
351 aux_symbol.symbol_expr(),
352 0,
353 function_symbol.location,
354 function_name,
355 symbol_table,
356 dest);
357
358 function.body.destructive_append(dest);
359
360 exprt return_expr =
361 typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type);
362
363 add_instruction(
364 goto_programt::make_set_return_value(std::move(return_expr)));
365
366 add_instruction(goto_programt::make_dead(aux_symbol.symbol_expr()));
367 }
368
369 add_instruction(goto_programt::make_end_function());
370
371 remove_skip(function.body);
372 }
373
374private:
375 const std::vector<irep_idt> globals_to_havoc;
380};
381
382class generate_function_bodies_errort : public std::runtime_error
383{
384public:
385 explicit generate_function_bodies_errort(const std::string &reason)
386 : runtime_error(reason)
387 {
388 }
389};
390
393std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
394 const std::string &options,
395 const c_object_factory_parameterst &object_factory_parameters,
396 const symbol_tablet &symbol_table,
397 message_handlert &message_handler)
398{
399 if(options.empty() || options == "nondet-return")
400 {
401 return util_make_unique<havoc_generate_function_bodiest>(
402 std::vector<irep_idt>{},
403 std::regex{},
404 object_factory_parameters,
405 message_handler);
406 }
407
408 if(options == "assume-false")
409 {
410 return util_make_unique<assume_false_generate_function_bodiest>();
411 }
412
413 if(options == "assert-false")
414 {
415 return util_make_unique<assert_false_generate_function_bodiest>();
416 }
417
418 if(options == "assert-false-assume-false")
419 {
420 return util_make_unique<
422 }
423
424 const std::vector<std::string> option_components = split_string(options, ',');
425 if(!option_components.empty() && option_components[0] == "havoc")
426 {
427 std::regex globals_regex;
428 std::regex params_regex;
429 std::vector<std::size_t> param_numbers;
430 for(std::size_t i = 1; i < option_components.size(); ++i)
431 {
432 const std::vector<std::string> key_value_pair =
433 split_string(option_components[i], ':');
434 if(key_value_pair.size() != 2)
435 {
437 "Expected key_value_pair of form argument:value");
438 }
439 if(key_value_pair[0] == "globals")
440 {
441 globals_regex = key_value_pair[1];
442 }
443 else if(key_value_pair[0] == "params")
444 {
445 auto param_identifiers = split_string(key_value_pair[1], ';');
446 if(param_identifiers.size() == 1)
447 {
448 auto maybe_nondet_param_number =
449 string2optional_size_t(param_identifiers.back());
450 if(!maybe_nondet_param_number.has_value())
451 {
452 params_regex = key_value_pair[1];
453 continue;
454 }
455 }
457 param_identifiers.begin(),
458 param_identifiers.end(),
459 std::back_inserter(param_numbers),
460 [](const std::string &param_id) {
461 auto maybe_nondet_param_number = string2optional_size_t(param_id);
462 INVARIANT(
463 maybe_nondet_param_number.has_value(),
464 param_id + " not a number");
465 return *maybe_nondet_param_number;
466 });
467 std::sort(param_numbers.begin(), param_numbers.end());
468 }
469 else
470 {
472 "Unknown option \"" + key_value_pair[0] + "\"");
473 }
474 }
475 std::vector<irep_idt> globals_to_havoc;
476 namespacet ns(symbol_table);
477 messaget messages(message_handler);
478 const std::regex cprover_prefix = std::regex("__CPROVER.*");
479 for(auto const &symbol : symbol_table.symbols)
480 {
481 if(
482 symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
483 std::regex_match(id2string(symbol.first), globals_regex))
484 {
485 if(std::regex_match(id2string(symbol.first), cprover_prefix))
486 {
487 messages.warning() << "generate function bodies: "
488 << "matched global '" << id2string(symbol.first)
489 << "' begins with __CPROVER, "
490 << "havoc-ing this global may interfere"
491 << " with analysis" << messaget::eom;
492 }
493 globals_to_havoc.push_back(symbol.first);
494 }
495 }
496 if(param_numbers.empty())
497 return util_make_unique<havoc_generate_function_bodiest>(
498 std::move(globals_to_havoc),
499 std::move(params_regex),
500 object_factory_parameters,
501 message_handler);
502 else
503 return util_make_unique<havoc_generate_function_bodiest>(
504 std::move(globals_to_havoc),
505 std::move(param_numbers),
506 object_factory_parameters,
507 message_handler);
508 }
509 throw generate_function_bodies_errort("Can't parse \"" + options + "\"");
510}
511
520 const std::regex &functions_regex,
521 const generate_function_bodiest &generate_function_body,
522 goto_modelt &model,
523 message_handlert &message_handler)
524{
525 messaget messages(message_handler);
526 const std::regex cprover_prefix = std::regex("__CPROVER.*");
527 bool did_generate_body = false;
528 for(auto &function : model.goto_functions.function_map)
529 {
530 if(
531 !function.second.body_available() &&
532 std::regex_match(id2string(function.first), functions_regex))
533 {
534 if(std::regex_match(id2string(function.first), cprover_prefix))
535 {
536 messages.warning() << "generate function bodies: matched function '"
537 << id2string(function.first)
538 << "' begins with __CPROVER "
539 << "the generated body for this function "
540 << "may interfere with analysis" << messaget::eom;
541 }
542 did_generate_body = true;
543 generate_function_body.generate_function_body(
544 function.second, model.symbol_table, function.first);
545 }
546 }
547 if(!did_generate_body)
548 {
549 messages.warning()
550 << "generate function bodies: No function name matched regex"
551 << messaget::eom;
552 }
553}
554
556 const std::string &function_name,
557 const std::string &call_site_id,
558 const generate_function_bodiest &generate_function_body,
559 goto_modelt &model,
560 message_handlert &message_handler)
561{
562 PRECONDITION(!has_prefix(function_name, CPROVER_PREFIX));
563 auto call_site_number = string2optional_size_t(call_site_id);
564 PRECONDITION(call_site_number.has_value());
565
566 messaget messages(message_handler);
567
568 bool found = false;
569 irep_idt function_mode;
570 typet function_type;
571
572 // get the mode and type from symbol table
573 for(auto const &symbol_pair : model.symbol_table)
574 {
575 auto const symbol = symbol_pair.second;
576 if(symbol.type.id() == ID_code && symbol.name == function_name)
577 {
578 function_mode = symbol.mode;
579 function_type = symbol.type;
580 found = true;
581 break;
582 }
583 }
584 CHECK_RETURN(found);
585
586 // add function of the right name to the symbol table
587 symbolt havoc_function_symbol{};
588 havoc_function_symbol.name = havoc_function_symbol.base_name =
589 havoc_function_symbol.pretty_name = function_name + "." + call_site_id;
590
591 havoc_function_symbol.is_lvalue = true;
592 havoc_function_symbol.mode = function_mode;
593 havoc_function_symbol.type = function_type;
594
595 model.symbol_table.insert(havoc_function_symbol);
596
597 auto const &generated_havoc =
598 model.symbol_table.lookup_ref(havoc_function_symbol.name);
599
600 // convert to get the function stub to goto-model
601 goto_convert(model.symbol_table, model.goto_functions, message_handler);
602
603 // now generate body as above
604 for(auto &function : model.goto_functions.function_map)
605 {
606 if(
607 !function.second.body_available() &&
608 havoc_function_symbol.name == id2string(function.first))
609 {
610 generate_function_body.generate_function_body(
611 function.second, model.symbol_table, function.first);
612 }
613 }
614
615 auto is_havoc_function_call = [&function_name](const exprt &expr) {
616 if(expr.id() != ID_symbol)
617 return false;
618 std::string called_function_name =
620 if(called_function_name == function_name)
621 return true;
622
623 return (has_prefix(called_function_name, function_name + "."));
624 };
625
626 // finally, rename the (right) call site
627 std::size_t counter = 0;
628 for(auto &function : model.goto_functions.function_map)
629 {
630 for(auto &instruction : function.second.body.instructions)
631 {
632 if(instruction.is_function_call())
633 {
634 auto &called_function =
635 to_code_function_call(instruction.code_nonconst()).function();
636 if(is_havoc_function_call(called_function))
637 {
638 if(++counter == *call_site_number)
639 {
640 called_function = generated_havoc.symbol_expr();
641 return;
642 }
643 }
644 }
645 }
646 }
647}
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
C Nondet Symbol Factory.
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:89
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
The Boolean constant false.
Definition: std_expr.h:2865
generate_function_bodies_errort(const std::string &reason)
Base class for replace_function_body implementations.
void generate_function_body(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Replace the function body with one based on the replace_function_body class being used.
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
virtual void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const =0
Produce a body for the passed function At this point the body of function is always empty,...
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
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
bool body_available() const
Definition: goto_function.h:35
void set_parameter_identifiers(const code_typet &code_type)
Definition: goto_function.h:40
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
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:863
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:956
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:949
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:996
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::vector< std::size_t > param_numbers_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
const std::vector< irep_idt > globals_to_havoc
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
bool should_havoc_param(const std::string &param_name, std::size_t param_number) const
optionalt< std::vector< std::size_t > > param_numbers_to_havoc
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
const c_object_factory_parameterst & object_factory_parameters
void havoc_expr_rec(const exprt &lhs, const std::size_t initial_depth, const source_locationt &source_location, const irep_idt &function_id, symbol_tablet &symbol_table, goto_programt &dest) const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
void remove(const irep_idt &name)
Definition: irep.cpp:96
const irep_idt & id() const
Definition: irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
message_handlert & get_message_handler()
Definition: message.h:184
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The null pointer constant.
Definition: pointer_expr.h:723
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Expression to hold a symbol (variable)
Definition: std_expr.h:80
void gen_nondet_init(code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett(), const bool assign_const=true)
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
std::set< irep_idt > recursion_sett
void declare_created_symbols(code_blockt &init_code)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(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
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
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 mode
Language mode.
Definition: symbol.h:49
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
static format_containert< T > format(const T &o)
Definition: format.h:37
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.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Program Transformation.
Goto Programs with Functions.
const code_function_callt & to_code_function_call(const codet &code)
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
optionalt< std::size_t > string2optional_size_t(const std::string &str, int base)
Convert string to size_t similar to the stoul or stoull functions, return nullopt when the conversion...
Definition: string2int.cpp:69
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)