cprover
generate_function_bodies.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Replace bodies of goto functions
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
10 
13 
17 
18 #include <util/arith_tools.h>
19 #include <util/format_expr.h>
20 #include <util/fresh_symbol.h>
21 #include <util/make_unique.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.type = to_code_type(function_symbol.type);
68  function.set_parameter_identifiers(to_code_type(function_symbol.type));
69 }
70 
72 {
73 protected:
75  goto_functiont &function,
76  symbol_tablet &symbol_table,
77  const irep_idt &function_name) const override
78  {
79  auto const &function_symbol = symbol_table.lookup_ref(function_name);
80  // NOLINTNEXTLINE
81  auto add_instruction = [&](goto_programt::instructiont &&i) {
82  auto instruction = function.body.add(std::move(i));
83  instruction->source_location = function_symbol.location;
84  return instruction;
85  };
86  add_instruction(goto_programt::make_assumption(false_exprt()));
87  add_instruction(goto_programt::make_end_function());
88  }
89 };
90 
92 {
93 protected:
95  goto_functiont &function,
96  symbol_tablet &symbol_table,
97  const irep_idt &function_name) const override
98  {
99  auto const &function_symbol = symbol_table.lookup_ref(function_name);
100  // NOLINTNEXTLINE
101  auto add_instruction = [&](goto_programt::instructiont &&i) {
102  auto instruction = function.body.add(std::move(i));
103  instruction->source_location = function_symbol.location;
104  instruction->source_location.set_function(function_name);
105  return instruction;
106  };
107  auto assert_instruction =
108  add_instruction(goto_programt::make_assertion(false_exprt()));
109  const namespacet ns(symbol_table);
110  std::ostringstream comment_stream;
111  comment_stream << id2string(ID_assertion) << " "
112  << format(assert_instruction->get_condition());
113  assert_instruction->source_location.set_comment(comment_stream.str());
114  assert_instruction->source_location.set_property_class(ID_assertion);
115  add_instruction(goto_programt::make_end_function());
116  }
117 };
118 
121 {
122 protected:
124  goto_functiont &function,
125  symbol_tablet &symbol_table,
126  const irep_idt &function_name) const override
127  {
128  auto const &function_symbol = symbol_table.lookup_ref(function_name);
129  // NOLINTNEXTLINE
130  auto add_instruction = [&](goto_programt::instructiont &&i) {
131  auto instruction = function.body.add(std::move(i));
132  instruction->source_location = function_symbol.location;
133  instruction->source_location.set_function(function_name);
134  return instruction;
135  };
136  auto assert_instruction =
137  add_instruction(goto_programt::make_assertion(false_exprt()));
138  const namespacet ns(symbol_table);
139  std::ostringstream comment_stream;
140  comment_stream << id2string(ID_assertion) << " "
141  << format(assert_instruction->get_condition());
142  assert_instruction->source_location.set_comment(comment_stream.str());
143  assert_instruction->source_location.set_property_class(ID_assertion);
144  add_instruction(goto_programt::make_assumption(false_exprt()));
145  add_instruction(goto_programt::make_end_function());
146  }
147 };
148 
150 {
151 public:
153  std::vector<irep_idt> globals_to_havoc,
154  std::regex parameters_to_havoc,
156  message_handlert &message_handler)
161  message(message_handler)
162  {
163  }
164 
166  std::vector<irep_idt> globals_to_havoc,
167  std::vector<std::size_t> param_numbers_to_havoc,
169  message_handlert &message_handler)
174  message(message_handler)
175  {
176  }
177 
178 private:
180  const exprt &lhs,
181  const std::size_t initial_depth,
182  const source_locationt &source_location,
183  const irep_idt &function_id,
184  symbol_tablet &symbol_table,
185  goto_programt &dest) const
186  {
187  symbol_factoryt symbol_factory(
188  symbol_table,
189  source_location,
190  function_id,
193 
194  code_blockt assignments;
195 
196  symbol_factory.gen_nondet_init(
197  assignments,
198  lhs,
199  initial_depth,
201  false); // do not initialize const objects at the top level
202 
203  code_blockt init_code;
204 
205  symbol_factory.declare_created_symbols(init_code);
206  init_code.append(assignments);
207 
208  goto_programt tmp_dest;
209  goto_convert(
210  init_code, symbol_table, tmp_dest, message.get_message_handler(), ID_C);
211 
212  dest.destructive_append(tmp_dest);
213  }
214 
216  const std::string &param_name,
217  std::size_t param_number) const
218  {
219  if(parameters_to_havoc.has_value())
220  {
221  return std::regex_match(param_name, *parameters_to_havoc);
222  }
223  else
224  {
226  return std::binary_search(
227  param_numbers_to_havoc->begin(),
228  param_numbers_to_havoc->end(),
229  param_number);
230  }
231  }
232 
233 protected:
235  goto_functiont &function,
236  symbol_tablet &symbol_table,
237  const irep_idt &function_name) const override
238  {
239  const namespacet ns(symbol_table);
240  // some user input checking
241  if(param_numbers_to_havoc.has_value() && !param_numbers_to_havoc->empty())
242  {
243  auto max_param_number = std::max_element(
245  if(*max_param_number >= function.parameter_identifiers.size())
246  {
248  "function " + id2string(function_name) + " does not take " +
249  std::to_string(*max_param_number + 1) + " arguments",
250  "--generate-havocing-body"};
251  }
252  for(const auto number : *param_numbers_to_havoc)
253  {
254  const auto &parameter = function.parameter_identifiers[number];
255  const symbolt &parameter_symbol = ns.lookup(parameter);
256  if(parameter_symbol.type.id() != ID_pointer)
257  {
259  "argument number " + std::to_string(number) + " of function " +
260  id2string(function_name) + " is not a pointer",
261  "--generate-havocing-body"};
262  }
263  }
264  }
265 
266  auto const &function_symbol = symbol_table.lookup_ref(function_name);
267  // NOLINTNEXTLINE
268  auto add_instruction = [&](goto_programt::instructiont &&i) {
269  auto instruction = function.body.add(std::move(i));
270  instruction->source_location = function_symbol.location;
271  return instruction;
272  };
273 
274  for(std::size_t i = 0; i < function.parameter_identifiers.size(); ++i)
275  {
276  const auto &parameter = function.parameter_identifiers[i];
277  const symbolt &parameter_symbol = ns.lookup(parameter);
278  if(
279  parameter_symbol.type.id() == ID_pointer &&
280  !parameter_symbol.type.subtype().get_bool(ID_C_constant) &&
281  should_havoc_param(id2string(parameter_symbol.base_name), i))
282  {
283  auto goto_instruction =
285  parameter_symbol.symbol_expr(),
286  null_pointer_exprt(to_pointer_type(parameter_symbol.type)))));
287 
288  dereference_exprt dereference_expr(
289  parameter_symbol.symbol_expr(), parameter_symbol.type.subtype());
290 
291  goto_programt dest;
293  dereference_expr,
294  1, // depth 1 since we pass the dereferenced pointer
295  function_symbol.location,
296  function_name,
297  symbol_table,
298  dest);
299 
300  function.body.destructive_append(dest);
301 
302  auto label_instruction = add_instruction(goto_programt::make_skip());
303  goto_instruction->complete_goto(label_instruction);
304  }
305  }
306 
307  for(auto const &global_id : globals_to_havoc)
308  {
309  auto const &global_sym = symbol_table.lookup_ref(global_id);
310 
311  goto_programt dest;
312 
314  symbol_exprt(global_sym.name, global_sym.type),
315  0,
316  function_symbol.location,
317  irep_idt(),
318  symbol_table,
319  dest);
320 
321  function.body.destructive_append(dest);
322  }
323 
324  if(function.type.return_type() != empty_typet())
325  {
326  typet type(function.type.return_type());
327  type.remove(ID_C_constant);
328 
329  symbolt &aux_symbol = get_fresh_aux_symbol(
330  type,
331  id2string(function_name),
332  "return_value",
333  function_symbol.location,
334  ID_C,
335  symbol_table);
336 
337  aux_symbol.is_static_lifetime = false;
338 
339  add_instruction(goto_programt::make_decl(aux_symbol.symbol_expr()));
340 
341  goto_programt dest;
342 
344  aux_symbol.symbol_expr(),
345  0,
346  function_symbol.location,
347  function_name,
348  symbol_table,
349  dest);
350 
351  function.body.destructive_append(dest);
352 
354  aux_symbol.symbol_expr(), function.type.return_type());
355 
356  add_instruction(goto_programt::make_return(code_returnt(return_expr)));
357 
358  add_instruction(goto_programt::make_dead(aux_symbol.symbol_expr()));
359  }
360 
361  add_instruction(goto_programt::make_end_function());
362 
363  remove_skip(function.body);
364  }
365 
366 private:
367  const std::vector<irep_idt> globals_to_havoc;
371  mutable messaget message;
372 };
373 
374 class generate_function_bodies_errort : public std::runtime_error
375 {
376 public:
377  explicit generate_function_bodies_errort(const std::string &reason)
378  : runtime_error(reason)
379  {
380  }
381 };
382 
385 std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
386  const std::string &options,
387  const c_object_factory_parameterst &object_factory_parameters,
388  const symbol_tablet &symbol_table,
389  message_handlert &message_handler)
390 {
391  if(options.empty() || options == "nondet-return")
392  {
393  return util_make_unique<havoc_generate_function_bodiest>(
394  std::vector<irep_idt>{},
395  std::regex{},
396  object_factory_parameters,
397  message_handler);
398  }
399 
400  if(options == "assume-false")
401  {
402  return util_make_unique<assume_false_generate_function_bodiest>();
403  }
404 
405  if(options == "assert-false")
406  {
407  return util_make_unique<assert_false_generate_function_bodiest>();
408  }
409 
410  if(options == "assert-false-assume-false")
411  {
412  return util_make_unique<
414  }
415 
416  const std::vector<std::string> option_components = split_string(options, ',');
417  if(!option_components.empty() && option_components[0] == "havoc")
418  {
419  std::regex globals_regex;
420  std::regex params_regex;
421  std::vector<std::size_t> param_numbers;
422  for(std::size_t i = 1; i < option_components.size(); ++i)
423  {
424  const std::vector<std::string> key_value_pair =
425  split_string(option_components[i], ':');
426  if(key_value_pair.size() != 2)
427  {
429  "Expected key_value_pair of form argument:value");
430  }
431  if(key_value_pair[0] == "globals")
432  {
433  globals_regex = key_value_pair[1];
434  }
435  else if(key_value_pair[0] == "params")
436  {
437  auto param_identifiers = split_string(key_value_pair[1], ';');
438  if(param_identifiers.size() == 1)
439  {
440  auto maybe_nondet_param_number =
441  string2optional_size_t(param_identifiers.back());
442  if(!maybe_nondet_param_number.has_value())
443  {
444  params_regex = key_value_pair[1];
445  continue;
446  }
447  }
448  std::transform(
449  param_identifiers.begin(),
450  param_identifiers.end(),
451  std::back_inserter(param_numbers),
452  [](const std::string &param_id) {
453  auto maybe_nondet_param_number = string2optional_size_t(param_id);
454  INVARIANT(
455  maybe_nondet_param_number.has_value(),
456  param_id + " not a number");
457  return *maybe_nondet_param_number;
458  });
459  std::sort(param_numbers.begin(), param_numbers.end());
460  }
461  else
462  {
464  "Unknown option \"" + key_value_pair[0] + "\"");
465  }
466  }
467  std::vector<irep_idt> globals_to_havoc;
468  namespacet ns(symbol_table);
469  messaget messages(message_handler);
470  const std::regex cprover_prefix = std::regex("__CPROVER.*");
471  for(auto const &symbol : symbol_table.symbols)
472  {
473  if(
474  symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
475  std::regex_match(id2string(symbol.first), globals_regex))
476  {
477  if(std::regex_match(id2string(symbol.first), cprover_prefix))
478  {
479  messages.warning() << "generate function bodies: "
480  << "matched global '" << id2string(symbol.first)
481  << "' begins with __CPROVER, "
482  << "havoc-ing this global may interfere"
483  << " with analysis" << messaget::eom;
484  }
485  globals_to_havoc.push_back(symbol.first);
486  }
487  }
488  if(param_numbers.empty())
489  return util_make_unique<havoc_generate_function_bodiest>(
490  std::move(globals_to_havoc),
491  std::move(params_regex),
492  object_factory_parameters,
493  message_handler);
494  else
495  return util_make_unique<havoc_generate_function_bodiest>(
496  std::move(globals_to_havoc),
497  std::move(param_numbers),
498  object_factory_parameters,
499  message_handler);
500  }
501  throw generate_function_bodies_errort("Can't parse \"" + options + "\"");
502 }
503 
512  const std::regex &functions_regex,
513  const generate_function_bodiest &generate_function_body,
514  goto_modelt &model,
515  message_handlert &message_handler)
516 {
517  messaget messages(message_handler);
518  const std::regex cprover_prefix = std::regex("__CPROVER.*");
519  bool did_generate_body = false;
520  for(auto &function : model.goto_functions.function_map)
521  {
522  if(
523  !function.second.body_available() &&
524  std::regex_match(id2string(function.first), functions_regex))
525  {
526  if(std::regex_match(id2string(function.first), cprover_prefix))
527  {
528  messages.warning() << "generate function bodies: matched function '"
529  << id2string(function.first)
530  << "' begins with __CPROVER "
531  << "the generated body for this function "
532  << "may interfere with analysis" << messaget::eom;
533  }
534  did_generate_body = true;
535  generate_function_body.generate_function_body(
536  function.second, model.symbol_table, function.first);
537  }
538  }
539  if(!did_generate_body)
540  {
541  messages.warning()
542  << "generate function bodies: No function name matched regex"
543  << messaget::eom;
544  }
545 }
546 
548  const std::string &function_name,
549  const std::string &call_site_id,
550  const generate_function_bodiest &generate_function_body,
551  goto_modelt &model,
552  message_handlert &message_handler)
553 {
554  PRECONDITION(!has_prefix(function_name, CPROVER_PREFIX));
555  auto call_site_number = string2optional_size_t(call_site_id);
556  PRECONDITION(call_site_number.has_value());
557 
558  messaget messages(message_handler);
559 
560  bool found = false;
561  irep_idt function_mode;
562  typet function_type;
563 
564  // get the mode and type from symbol table
565  for(auto const &symbol_pair : model.symbol_table)
566  {
567  auto const symbol = symbol_pair.second;
568  if(symbol.type.id() == ID_code && symbol.name == function_name)
569  {
570  function_mode = symbol.mode;
571  function_type = symbol.type;
572  found = true;
573  break;
574  }
575  }
576  CHECK_RETURN(found);
577 
578  // add function of the right name to the symbol table
579  symbolt havoc_function_symbol{};
580  havoc_function_symbol.name = havoc_function_symbol.base_name =
581  havoc_function_symbol.pretty_name = function_name + "." + call_site_id;
582 
583  havoc_function_symbol.is_lvalue = true;
584  havoc_function_symbol.mode = function_mode;
585  havoc_function_symbol.type = function_type;
586 
587  model.symbol_table.insert(havoc_function_symbol);
588 
589  auto const &generated_havoc =
590  model.symbol_table.lookup_ref(havoc_function_symbol.name);
591 
592  // convert to get the function stub to goto-model
593  model.goto_functions.function_map[havoc_function_symbol.name].type =
594  to_code_type(generated_havoc.type);
595  goto_convert(model.symbol_table, model.goto_functions, message_handler);
596 
597  // now generate body as above
598  for(auto &function : model.goto_functions.function_map)
599  {
600  if(
601  !function.second.body_available() &&
602  havoc_function_symbol.name == id2string(function.first))
603  {
604  generate_function_body.generate_function_body(
605  function.second, model.symbol_table, function.first);
606  }
607  }
608 
609  auto is_havoc_function_call = [&function_name](const exprt &expr) {
610  if(expr.id() != ID_symbol)
611  return false;
612  std::string called_function_name =
613  id2string(to_symbol_expr(expr).get_identifier());
614  if(called_function_name == function_name)
615  return true;
616 
617  return (has_prefix(called_function_name, function_name + "."));
618  };
619 
620  // finally, rename the (right) call site
621  std::size_t counter = 0;
622  for(auto &function : model.goto_functions.function_map)
623  {
624  for(auto &instruction : function.second.body.instructions)
625  {
626  if(instruction.is_function_call())
627  {
628  auto &called_function =
629  to_code_function_call(instruction.code).function();
630  if(is_havoc_function_call(called_function))
631  {
632  if(++counter == *call_site_number)
633  {
634  called_function = generated_havoc.symbol_expr();
635  return;
636  }
637  }
638  }
639  }
640  }
641 }
c_nondet_symbol_factory.h
C Nondet Symbol Factory.
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
format
static format_containert< T > format(const T &o)
Definition: format.h:35
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
generate_function_bodiest::generate_function_body
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.
Definition: generate_function_bodies.cpp:26
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
havoc_generate_function_bodiest::param_numbers_to_havoc
optionalt< std::vector< std::size_t > > param_numbers_to_havoc
Definition: generate_function_bodies.cpp:369
arith_tools.h
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
assert_false_then_assume_false_generate_function_bodiest::generate_function_body_impl
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,...
Definition: generate_function_bodies.cpp:123
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
assert_false_generate_function_bodiest
Definition: generate_function_bodies.cpp:92
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
prefix.h
generate_function_bodiest::generate_function_body_impl
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,...
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
generate_function_bodies
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-...
Definition: generate_function_bodies.cpp:511
generate_function_bodiest
Base class for replace_function_body implementations.
Definition: generate_function_bodies.h:25
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
goto_convert.h
Program Transformation.
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
equal_exprt
Equality.
Definition: std_expr.h:1190
generate_function_bodies.h
havoc_generate_function_bodiest::parameters_to_havoc
optionalt< std::regex > parameters_to_havoc
Definition: generate_function_bodies.cpp:368
generate_function_bodies_errort::generate_function_bodies_errort
generate_function_bodies_errort(const std::string &reason)
Definition: generate_function_bodies.cpp:377
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1846
generate_function_bodies_errort
Definition: generate_function_bodies.cpp:375
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
string2int.h
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
havoc_generate_function_bodiest::object_factory_parameters
const c_object_factory_parameterst & object_factory_parameters
Definition: generate_function_bodies.cpp:370
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
make_unique.h
c_object_factory_parameters.h
assume_false_generate_function_bodiest::generate_function_body_impl
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,...
Definition: generate_function_bodies.cpp:74
havoc_generate_function_bodiest::havoc_expr_rec
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
Definition: generate_function_bodies.cpp:179
empty_typet
The empty type.
Definition: std_types.h:46
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:15
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
havoc_generate_function_bodiest::havoc_generate_function_bodiest
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)
Definition: generate_function_bodies.cpp:165
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
havoc_generate_function_bodiest::generate_function_body_impl
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,...
Definition: generate_function_bodies.cpp:234
assert_false_generate_function_bodiest::generate_function_body_impl
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,...
Definition: generate_function_bodies.cpp:94
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
assume_false_generate_function_bodiest
Definition: generate_function_bodies.cpp:72
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
string2optional_size_t
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:72
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
havoc_generate_function_bodiest
Definition: generate_function_bodies.cpp:150
havoc_generate_function_bodiest::globals_to_havoc
const std::vector< irep_idt > globals_to_havoc
Definition: generate_function_bodies.cpp:367
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
havoc_generate_function_bodiest::message
messaget message
Definition: generate_function_bodies.cpp:371
assert_false_then_assume_false_generate_function_bodiest
Definition: generate_function_bodies.cpp:121
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:838
source_locationt
Definition: source_location.h:20
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
symbol_factoryt::gen_nondet_init
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 ...
Definition: c_nondet_symbol_factory.cpp:37
format_expr.h
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
havoc_generate_function_bodiest::havoc_generate_function_bodiest
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)
Definition: generate_function_bodies.cpp:152
symbolt
Symbol table entry.
Definition: symbol.h:28
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:87
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
havoc_generate_function_bodiest::should_havoc_param
bool should_havoc_param(const std::string &param_name, std::size_t param_number) const
Definition: generate_function_bodies.cpp:215
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
lifetimet::DYNAMIC
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
generate_function_bodies_factory
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.
Definition: generate_function_bodies.cpp:385
symbol_factoryt
Definition: c_nondet_symbol_factory.h:25
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
symbol_factoryt::recursion_sett
std::set< irep_idt > recursion_sett
Definition: c_nondet_symbol_factory.h:36
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:184
generate_function_bodiest::generate_parameter_names
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
Definition: generate_function_bodies.cpp:36
goto_convert_functions.h
Goto Programs with Functions.
remove_skip.h
Program Transformation.
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
messaget::warning
mstreamt & warning() const
Definition: message.h:404
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
get_fresh_aux_symbol
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 ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:967
symbol_factoryt::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Definition: c_nondet_symbol_factory.h:65