cprover
function_call_harness_generator.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: harness generator for functions
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
11 #include <util/allocate_objects.h>
12 #include <util/arith_tools.h>
13 #include <util/c_types.h>
14 #include <util/exception_utils.h>
15 #include <util/prefix.h>
16 #include <util/std_code.h>
17 #include <util/std_expr.h>
18 #include <util/string2int.h>
19 #include <util/string_utils.h>
20 #include <util/ui_message.h>
21 
24 
25 #include <algorithm>
26 #include <iterator>
27 #include <set>
28 
32 
36 /* NOLINTNEXTLINE(readability/identifier_spacing) */
38 {
40  irep_idt function;
44  bool nondet_globals = false;
45 
47  std::unique_ptr<recursive_initializationt> recursive_initialization;
48 
51 
52  std::vector<std::set<irep_idt>> function_parameters_to_treat_equal;
53  std::vector<std::set<irep_idt>> function_arguments_to_treat_equal;
54 
57 
58  std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
59  std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
60 
61  std::set<symbol_exprt> global_pointers;
62 
64  void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
67  void generate_nondet_globals(code_blockt &function_body);
71  void generate_initialisation_code_for(code_blockt &block, const exprt &lhs);
81  void call_function(
82  const code_function_callt::argumentst &arguments,
83  code_blockt &function_body);
92  std::unordered_set<irep_idt>
94 };
95 
97  ui_message_handlert &message_handler)
98  : goto_harness_generatort{}, p_impl(util_make_unique<implt>())
99 {
100  p_impl->message_handler = &message_handler;
101 }
102 
104 
106  const std::string &option,
107  const std::list<std::string> &values)
108 {
111 
112  if(p_impl->recursive_initialization_config.handle_option(option, values))
113  {
114  // the option belongs to recursive initialization
115  }
116  else if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
117  {
118  p_impl->function = require_exactly_one_value(option, values);
119  }
121  {
122  p_impl->nondet_globals = true;
123  }
125  {
126  p_impl->function_parameters_to_treat_as_arrays.insert(
127  values.begin(), values.end());
128  }
130  {
131  for(auto const &value : values)
132  {
133  for(auto const &param_cluster : split_string(value, ';'))
134  {
135  std::set<irep_idt> equal_param_set;
136  for(auto const &param_id : split_string(param_cluster, ','))
137  {
138  equal_param_set.insert(param_id);
139  }
140  p_impl->function_parameters_to_treat_equal.push_back(equal_param_set);
141  }
142  }
143  }
145  {
146  for(auto const &array_size_pair : values)
147  {
148  try
149  {
150  std::string array;
151  std::string size;
152  split_string(array_size_pair, ':', array, size);
153  // --associated-array-size implies --treat-pointer-as-array
154  // but it is not an error to specify both, so we don't check
155  // for duplicates here
156  p_impl->function_parameters_to_treat_as_arrays.insert(array);
157  auto const inserted =
158  p_impl->function_parameter_to_associated_array_size.emplace(
159  array, size);
160  if(!inserted.second)
161  {
163  "can not have two associated array sizes for one array",
165  }
166  }
167  catch(const deserialization_exceptiont &)
168  {
170  "'" + array_size_pair +
171  "' is in an invalid format for array size pair",
173  "array_name:size_name, where both are the names of function "
174  "parameters"};
175  }
176  }
177  }
179  {
180  p_impl->function_parameters_to_treat_as_cstrings.insert(
181  values.begin(), values.end());
182  }
184  {
185  p_impl->recursive_initialization_config.arguments_may_be_equal = true;
186  }
188  {
189  std::transform(
190  values.begin(),
191  values.end(),
192  std::inserter(
193  p_impl->recursive_initialization_config
194  .potential_null_function_pointers,
195  p_impl->recursive_initialization_config.potential_null_function_pointers
196  .end()),
197  [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
198  }
200  {
201  std::transform(
202  values.begin(),
203  values.end(),
204  std::inserter(
205  p_impl->recursive_initialization_config
206  .potential_null_function_pointers,
207  p_impl->recursive_initialization_config.potential_null_function_pointers
208  .end()),
209  [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
210  }
211  else
212  {
214  "function harness generator cannot handle this option", "--" + option};
215  }
216 }
217 
219  goto_modelt &goto_model,
220  const irep_idt &harness_function_name)
221 {
222  p_impl->generate(goto_model, harness_function_name);
223 }
224 
226  goto_modelt &goto_model,
227  const irep_idt &harness_function_name)
228 {
229  symbol_table = &goto_model.symbol_table;
230  goto_functions = &goto_model.goto_functions;
231  this->harness_function_name = harness_function_name;
234 
235  // create body for the function
236  code_blockt function_body{};
237  auto const arguments = declare_arguments(function_body);
238 
239  // configure and create recursive initialisation object
247  for(const auto &pair : function_argument_to_associated_array_size)
248  {
250  pair.second);
251  }
256  recursive_initialization = util_make_unique<recursive_initializationt>(
257  recursive_initialization_config, goto_model);
258 
259  generate_nondet_globals(function_body);
260  call_function(arguments, function_body);
261  for(const auto &global_pointer : global_pointers)
262  {
263  recursive_initialization->free_if_possible(global_pointer, function_body);
264  }
265  recursive_initialization->free_cluster_origins(function_body);
266  add_harness_function_to_goto_model(std::move(function_body));
267 }
268 
270  code_blockt &function_body)
271 {
272  if(nondet_globals)
273  {
274  // generating initialisation code may introduce new globals
275  // i.e. modify the symbol table.
276  // Modifying the symbol table while iterating over it is not
277  // a good idea, therefore we just collect the names of globals
278  // we need to initialise first and then generate the
279  // initialisation code for all of them.
280  auto globals = std::vector<symbol_exprt>{};
281  for(const auto &symbol_table_entry : *symbol_table)
282  {
283  const auto &symbol = symbol_table_entry.second;
285  {
286  globals.push_back(symbol.symbol_expr());
287  }
288  }
289  for(auto const &global : globals)
290  {
291  generate_initialisation_code_for(function_body, global);
292  }
293  }
294 }
295 
297  code_blockt &block,
298  const exprt &lhs)
299 {
300  recursive_initialization->initialize(
301  lhs, from_integer(0, signed_int_type()), block);
302  if(recursive_initialization->needs_freeing(lhs))
303  global_pointers.insert(to_symbol_expr(lhs));
304 }
305 
307  const goto_modelt &goto_model)
308 {
309  if(p_impl->function == ID_empty_string)
311  "required parameter entry function not set",
313  if(
314  p_impl->recursive_initialization_config.min_dynamic_array_size >
315  p_impl->recursive_initialization_config.max_dynamic_array_size)
316  {
318  "min dynamic array size cannot be greater than max dynamic array size",
321  }
322 
323  const auto function_to_call_pointer =
324  goto_model.symbol_table.lookup(p_impl->function);
325  if(function_to_call_pointer == nullptr)
326  {
328  "entry function `" + id2string(p_impl->function) +
329  "' does not exist in the symbol table",
331  }
332  const auto &function_to_call = *function_to_call_pointer;
333  const auto &ftype = to_code_type(function_to_call.type);
334  for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal)
335  {
336  for(auto const &pointer_id : equal_cluster)
337  {
338  std::string decorated_pointer_id =
339  id2string(p_impl->function) + "::" + id2string(pointer_id);
340  bool is_a_param = false;
341  typet common_type = empty_typet{};
342  for(auto const &formal_param : ftype.parameters())
343  {
344  if(formal_param.get_identifier() == decorated_pointer_id)
345  {
346  is_a_param = true;
347  if(formal_param.type().id() != ID_pointer)
348  {
350  id2string(pointer_id) + " is not a pointer parameter",
352  }
353  if(common_type.id() != ID_empty)
354  {
355  if(common_type != formal_param.type())
356  {
358  "pointer arguments of conflicting type",
360  }
361  }
362  else
363  common_type = formal_param.type();
364  }
365  }
366  if(!is_a_param)
367  {
369  id2string(pointer_id) + " is not a parameter",
371  }
372  }
373  }
374 
375  const namespacet ns{goto_model.symbol_table};
376 
377  // Make sure all function pointers that the user asks are nullable are
378  // present in the symbol table.
379  for(const auto &nullable :
380  p_impl->recursive_initialization_config.potential_null_function_pointers)
381  {
382  const auto &function_pointer_symbol_pointer =
383  goto_model.symbol_table.lookup(nullable);
384 
385  if(function_pointer_symbol_pointer == nullptr)
386  {
388  "nullable function pointer `" + id2string(nullable) +
389  "' not found in symbol table",
391  }
392 
393  const auto &function_pointer_type =
394  ns.follow(function_pointer_symbol_pointer->type);
395 
396  if(!can_cast_type<pointer_typet>(function_pointer_type))
397  {
399  "`" + id2string(nullable) + "' is not a pointer",
401  }
402 
404  to_pointer_type(function_pointer_type).subtype()))
405  {
407  "`" + id2string(nullable) + "' is not pointing to a function",
409  }
410  }
411 }
412 
413 const symbolt &
415 {
416  auto function_found = symbol_table->lookup(function);
417 
418  if(function_found == nullptr)
419  {
421  "function that should be harnessed is not found " + id2string(function),
423  }
424 
425  return *function_found;
426 }
427 
430 {
431  if(symbol_table->lookup(harness_function_name))
432  {
434  "harness function already exists in the symbol table",
436  }
437 }
438 
441 {
442  const auto &function_to_call = lookup_function_to_call();
443 
444  // create the function symbol
445  symbolt harness_function_symbol{};
446  harness_function_symbol.name = harness_function_symbol.base_name =
447  harness_function_symbol.pretty_name = harness_function_name;
448 
449  harness_function_symbol.is_lvalue = true;
450  harness_function_symbol.mode = function_to_call.mode;
451  harness_function_symbol.type = code_typet{{}, empty_typet{}};
452  harness_function_symbol.value = std::move(function_body);
453 
454  symbol_table->insert(harness_function_symbol);
455 
456  auto const &generated_harness =
457  symbol_table->lookup_ref(harness_function_name);
458  goto_functions->function_map[harness_function_name].type =
459  to_code_type(generated_harness.type);
460  goto_convert(*symbol_table, *goto_functions, *message_handler);
461 }
462 
465  code_blockt &function_body)
466 {
467  const auto &function_to_call = lookup_function_to_call();
468  const auto &function_type = to_code_type(function_to_call.type);
469  const auto &parameters = function_type.parameters();
470 
471  code_function_callt::operandst arguments{};
472 
473  auto allocate_objects = allocate_objectst{function_to_call.mode,
474  function_to_call.location,
475  "__goto_harness",
476  *symbol_table};
477  std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
478  for(const auto &parameter : parameters)
479  {
480  auto argument = allocate_objects.allocate_automatic_local_object(
481  remove_const(parameter.type()), parameter.get_base_name());
482  parameter_name_to_argument_name.insert(
483  {parameter.get_base_name(), argument.get_identifier()});
484  arguments.push_back(argument);
485  }
486 
487  for(const auto &pair : parameter_name_to_argument_name)
488  {
489  auto const &parameter_name = pair.first;
490  auto const &argument_name = pair.second;
491  if(function_parameters_to_treat_as_arrays.count(parameter_name) != 0)
492  {
493  function_arguments_to_treat_as_arrays.insert(argument_name);
494  }
495 
496  if(function_parameters_to_treat_as_cstrings.count(parameter_name) != 0)
497  {
498  function_arguments_to_treat_as_cstrings.insert(argument_name);
499  }
500 
501  auto it = function_parameter_to_associated_array_size.find(parameter_name);
502  if(it != function_parameter_to_associated_array_size.end())
503  {
504  auto const &associated_array_size_parameter = it->second;
505  auto associated_array_size_argument =
506  parameter_name_to_argument_name.find(associated_array_size_parameter);
507  if(
508  associated_array_size_argument == parameter_name_to_argument_name.end())
509  {
511  "could not find parameter to associate the array size of array \"" +
512  id2string(parameter_name) + "\" (Expected parameter: \"" +
513  id2string(associated_array_size_parameter) + "\" on function \"" +
514  id2string(function_to_call.display_name()) + "\" in " +
515  function_to_call.location.as_string() + ")",
517  }
518  function_argument_to_associated_array_size.insert(
519  {argument_name, associated_array_size_argument->second});
520  }
521  }
522 
523  // translate the parameter to argument also in the equality clusters
524  for(auto const &equal_cluster : function_parameters_to_treat_equal)
525  {
526  std::set<irep_idt> cluster_argument_names;
527  for(auto const &parameter_name : equal_cluster)
528  {
529  INVARIANT(
530  parameter_name_to_argument_name.count(parameter_name) != 0,
531  id2string(parameter_name) + " is not a parameter");
532  cluster_argument_names.insert(
533  parameter_name_to_argument_name[parameter_name]);
534  }
535  function_arguments_to_treat_equal.push_back(cluster_argument_names);
536  }
537 
538  allocate_objects.declare_created_symbols(function_body);
539  return arguments;
540 }
541 
543  const code_function_callt::argumentst &arguments,
544  code_blockt &function_body)
545 {
546  auto const &function_to_call = lookup_function_to_call();
547  for(auto const &argument : arguments)
548  {
549  generate_initialisation_code_for(function_body, argument);
550  if(recursive_initialization->needs_freeing(argument))
551  global_pointers.insert(to_symbol_expr(argument));
552  }
553  code_function_callt function_call{function_to_call.symbol_expr(),
554  std::move(arguments)};
555  function_call.add_source_location() = function_to_call.location;
556 
557  function_body.add(std::move(function_call));
558 }
559 
560 std::unordered_set<irep_idt> function_call_harness_generatort::implt::
562 {
563  std::unordered_set<irep_idt> nullables;
564  for(const auto &nullable :
565  recursive_initialization_config.potential_null_function_pointers)
566  {
567  const auto &nullable_name = id2string(nullable);
568  const auto &function_prefix = id2string(function) + "::";
569  if(has_prefix(nullable_name, function_prefix))
570  {
571  nullables.insert(
572  "__goto_harness::" + nullable_name.substr(function_prefix.size()));
573  }
574  else
575  {
576  nullables.insert(nullable_name);
577  }
578  }
579  return nullables;
580 }
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
recursive_initialization_configt::pointers_to_treat_as_cstrings
std::set< irep_idt > pointers_to_treat_as_cstrings
Definition: recursive_initialization.h:41
GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
Definition: goto_harness_generator_factory.h:20
function_call_harness_generatort::implt::global_pointers
std::set< symbol_exprt > global_pointers
Definition: function_call_harness_generator.cpp:61
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
Definition: common_harness_generator_options.h:17
function_call_harness_generatort::implt::recursive_initialization
std::unique_ptr< recursive_initializationt > recursive_initialization
Definition: function_call_harness_generator.cpp:47
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
function_call_harness_generatort::implt::lookup_function_to_call
const symbolt & lookup_function_to_call()
Return a reference to the entry function or throw if it doesn't exist.
Definition: function_call_harness_generator.cpp:414
function_call_harness_generatort::validate_options
void validate_options(const goto_modelt &goto_model) override
Check if options are in a sane state, throw otherwise.
Definition: function_call_harness_generator.cpp:306
ui_message_handlert
Definition: ui_message.h:20
arith_tools.h
function_call_harness_generatort::function_call_harness_generatort
function_call_harness_generatort(ui_message_handlert &message_handler)
Definition: function_call_harness_generator.cpp:96
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
recursive_initialization.h
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
function_call_harness_generator.h
prefix.h
goto_model.h
Symbol Table + CFG.
recursive_initialization_configt::array_name_to_associated_array_size_variable
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
Definition: recursive_initialization.h:39
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
function_harness_generator_options.h
function_call_harness_generatort::implt::harness_function_name
irep_idt harness_function_name
Definition: function_call_harness_generator.cpp:41
harness_options_parser::require_exactly_one_value
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...
Definition: goto_harness_generator.cpp:21
recursive_initialization_configt::mode
irep_idt mode
Definition: recursive_initialization.h:30
goto_harness_generatort
Definition: goto_harness_generator.h:42
function_call_harness_generatort::implt::declare_arguments
code_function_callt::argumentst declare_arguments(code_blockt &function_body)
Declare local variables for each of the parameters of the entry function and return them.
Definition: function_call_harness_generator.cpp:464
function_call_harness_generatort::implt::symbol_table
symbol_tablet * symbol_table
Definition: function_call_harness_generator.cpp:42
FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT
Definition: function_harness_generator_options.h:16
goto_harness_parse_options.h
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
recursive_initialization_configt::pointers_to_treat_as_arrays
std::set< irep_idt > pointers_to_treat_as_arrays
Definition: recursive_initialization.h:37
remove_const
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
function_call_harness_generatort::implt::function_parameters_to_treat_as_arrays
std::set< irep_idt > function_parameters_to_treat_as_arrays
Definition: function_call_harness_generator.cpp:49
FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING
Definition: function_harness_generator_options.h:22
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
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
can_cast_type< code_typet >
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:933
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT
Definition: function_harness_generator_options.h:24
empty_typet
The empty type.
Definition: std_types.h:46
function_call_harness_generatort::implt::generate
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
Definition: function_call_harness_generator.cpp:225
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
recursive_initialization_configt::potential_null_function_pointers
std::unordered_set< irep_idt > potential_null_function_pointers
Definition: recursive_initialization.h:31
function_call_harness_generatort::implt::map_function_parameters_to_function_argument_names
std::unordered_set< irep_idt > map_function_parameters_to_function_argument_names()
For function parameters that are pointers to functions we want to be able to specify whether or not t...
Definition: function_call_harness_generator.cpp:561
FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT
#define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT
Definition: function_harness_generator_options.h:15
function_to_call
code_function_callt function_to_call(symbol_tablet &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:21
FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT
#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT
Definition: function_harness_generator_options.h:20
function_call_harness_generatort::implt::message_handler
ui_message_handlert * message_handler
Definition: function_call_harness_generator.cpp:39
function_call_harness_generatort::implt::recursive_initialization_config
recursive_initialization_configt recursive_initialization_config
Definition: function_call_harness_generator.cpp:46
function_call_harness_generatort::~function_call_harness_generatort
~function_call_harness_generatort() override
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
function_call_harness_generatort::implt::function_parameter_to_associated_array_size
std::map< irep_idt, irep_idt > function_parameter_to_associated_array_size
Definition: function_call_harness_generator.cpp:59
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
function_call_harness_generatort::p_impl
std::unique_ptr< implt > p_impl
Definition: function_call_harness_generator.h:42
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
std_code.h
function_call_harness_generatort::implt::function_parameters_to_treat_equal
std::vector< std::set< irep_idt > > function_parameters_to_treat_equal
Definition: function_call_harness_generator.cpp:52
function_call_harness_generatort::handle_option
void handle_option(const std::string &option, const std::list< std::string > &values) override
Handle a command line argument.
Definition: function_call_harness_generator.cpp:105
recursive_initialization_configt::variables_that_hold_array_sizes
std::set< irep_idt > variables_that_hold_array_sizes
Definition: recursive_initialization.h:38
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1513
FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT
#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT
Definition: function_harness_generator_options.h:14
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
function_call_harness_generatort::implt::function_arguments_to_treat_as_cstrings
std::set< irep_idt > function_arguments_to_treat_as_cstrings
Definition: function_call_harness_generator.cpp:56
function_call_harness_generatort::implt::function_parameters_to_treat_as_cstrings
std::set< irep_idt > function_parameters_to_treat_as_cstrings
Definition: function_call_harness_generator.cpp:55
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
function_call_harness_generatort::implt
This contains implementation details of function call harness generator to avoid leaking them out int...
Definition: function_call_harness_generator.cpp:38
COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
Definition: common_harness_generator_options.h:15
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
function_call_harness_generatort::implt::goto_functions
goto_functionst * goto_functions
Definition: function_call_harness_generator.cpp:43
function_call_harness_generatort::implt::generate_nondet_globals
void generate_nondet_globals(code_blockt &function_body)
Iterate over the symbol table and generate initialisation code for globals into the function body.
Definition: function_call_harness_generator.cpp:269
function_call_harness_generatort::implt::function_arguments_to_treat_equal
std::vector< std::set< irep_idt > > function_arguments_to_treat_equal
Definition: function_call_harness_generator.cpp:53
recursive_initialization_configt
Definition: recursive_initialization.h:27
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
allocate_objectst
Definition: allocate_objects.h:31
function_call_harness_generatort::implt::nondet_globals
bool nondet_globals
Definition: function_call_harness_generator.cpp:44
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_convert_functions.h
Goto Programs with Functions.
function_call_harness_generatort::generate
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
Generate a harness according to the set options.
Definition: function_call_harness_generator.cpp:218
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
function_call_harness_generatort::implt::ensure_harness_does_not_already_exist
void ensure_harness_does_not_already_exist()
Throw if the harness function already exists in the symbol table.
Definition: function_call_harness_generator.cpp:429
COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
Definition: common_harness_generator_options.h:16
function_call_harness_generatort::implt::function_argument_to_associated_array_size
std::map< irep_idt, irep_idt > function_argument_to_associated_array_size
Definition: function_call_harness_generator.cpp:58
recursive_initializationt::is_initialization_allowed
static bool is_initialization_allowed(const symbolt &symbol)
Definition: recursive_initialization.h:106
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
std_expr.h
API to expression classes.
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
allocate_objects.h
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
function_call_harness_generatort::implt::generate_initialisation_code_for
void generate_initialisation_code_for(code_blockt &block, const exprt &lhs)
Generate initialisation code for one lvalue inside block.
Definition: function_call_harness_generator.cpp:296
validation_modet::INVARIANT
@ INVARIANT
FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT
Definition: function_harness_generator_options.h:18
function_call_harness_generatort::implt::add_harness_function_to_goto_model
void add_harness_function_to_goto_model(code_blockt function_body)
Update the goto-model with the new harness function.
Definition: function_call_harness_generator.cpp:440
recursive_initialization_configt::pointers_to_treat_equal
std::vector< std::set< irep_idt > > pointers_to_treat_equal
Definition: recursive_initialization.h:42
function_call_harness_generatort::implt::function_arguments_to_treat_as_arrays
std::set< irep_idt > function_arguments_to_treat_as_arrays
Definition: function_call_harness_generator.cpp:50
function_call_harness_generatort::implt::call_function
void call_function(const code_function_callt::argumentst &arguments, code_blockt &function_body)
Write initialisation code for each of the arguments into function_body, then insert a call to the ent...
Definition: function_call_harness_generator.cpp:542
ui_message.h