92 std::unordered_set<irep_idt>
100 p_impl->message_handler = &message_handler;
106 const std::string &option,
107 const std::list<std::string> &values)
109 auto &require_exactly_one_value =
112 if(
p_impl->recursive_initialization_config.handle_option(option, values))
118 p_impl->function = require_exactly_one_value(option, values);
122 p_impl->nondet_globals =
true;
126 p_impl->function_parameters_to_treat_as_arrays.insert(
127 values.begin(), values.end());
131 for(
auto const &value : values)
140 p_impl->function_parameters_to_treat_equal.push_back(
157 p_impl->function_parameters_to_treat_as_arrays.insert(array);
158 auto const inserted =
159 p_impl->function_parameter_to_associated_array_size.emplace(
164 "can not have two associated array sizes for one array",
172 "' is in an invalid format for array size pair",
174 "array_name:size_name, where both are the names of function "
181 p_impl->function_parameters_to_treat_as_cstrings.insert(
182 values.begin(), values.end());
186 p_impl->recursive_initialization_config.arguments_may_be_equal =
true;
194 p_impl->recursive_initialization_config
195 .potential_null_function_pointers,
196 p_impl->recursive_initialization_config.potential_null_function_pointers
198 [](
const std::string &
opt) ->
irep_idt { return irep_idt{opt}; });
206 p_impl->recursive_initialization_config
207 .potential_null_function_pointers,
208 p_impl->recursive_initialization_config.potential_null_function_pointers
210 [](
const std::string &
opt) ->
irep_idt { return irep_idt{opt}; });
215 "function harness generator cannot handle this option",
"--" + option};
221 const irep_idt &harness_function_name)
223 p_impl->generate(goto_model, harness_function_name);
228 const irep_idt &harness_function_name)
281 auto globals = std::vector<symbol_exprt>{};
287 globals.push_back(symbol.symbol_expr());
303 if(recursive_initialization->needs_freeing(lhs))
312 "required parameter entry function not set",
315 p_impl->recursive_initialization_config.min_dynamic_array_size >
316 p_impl->recursive_initialization_config.max_dynamic_array_size)
319 "min dynamic array size cannot be greater than max dynamic array size",
330 "' does not exist in the symbol table",
359 "pointer arguments of conflicting type",
381 p_impl->recursive_initialization_config.potential_null_function_pointers)
390 "' not found in symbol table",
421 "function that should be harnessed is not found " +
id2string(function),
431 if(symbol_table->lookup(harness_function_name))
434 "harness function already exists in the symbol table",
456 goto_convert(*symbol_table, *goto_functions, *message_handler);
465 const auto ¶meters = function_type.parameters();
476 auto argument = allocate_objects.allocate_automatic_local_object(
487 if(function_parameters_to_treat_as_arrays.count(
parameter_name) != 0)
492 if(function_parameters_to_treat_as_cstrings.count(
parameter_name) != 0)
494 function_arguments_to_treat_as_cstrings.insert(
argument_name);
497 auto it = function_parameter_to_associated_array_size.find(
parameter_name);
498 if(it != function_parameter_to_associated_array_size.end())
507 "could not find parameter to associate the array size of array \"" +
514 function_argument_to_associated_array_size.insert(
520 for(
auto const &
equal_cluster : function_parameters_to_treat_equal)
531 function_arguments_to_treat_equal.push_back(
544 for(
auto const &
argument : arguments)
547 if(recursive_initialization->needs_freeing(
argument))
551 std::move(arguments)};
562 recursive_initialization_config.potential_null_function_pointers)
signedbv_typet signed_int_type()
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A codet representing sequential composition of program statements.
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
source_locationt & add_source_location()
void validate_options(const goto_modelt &goto_model) override
Check if options are in a sane state, throw otherwise.
~function_call_harness_generatort() override
std::unique_ptr< implt > p_impl
function_call_harness_generatort(ui_message_handlert &message_handler)
void handle_option(const std::string &option, const std::list< std::string > &values) override
Handle a command line argument.
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
Generate a harness according to the set options.
A collection of goto functions.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static bool is_initialization_allowed(const symbolt &symbol)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The type of an expression, extends irept.
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
bool has_prefix(const std::string &s, const std::string &prefix)
code_function_callt function_to_call(symbol_table_baset &symbol_table, const irep_idt &id, const irep_idt &argument)
#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT
#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT
#define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
const std::string & id2string(const irep_idt &d)
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...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
This contains implementation details of function call harness generator to avoid leaking them out int...
std::set< irep_idt > function_parameters_to_treat_as_arrays
symbol_tablet * symbol_table
goto_functionst * goto_functions
std::set< symbol_exprt > global_pointers
std::set< irep_idt > function_arguments_to_treat_as_arrays
irep_idt harness_function_name
std::map< irep_idt, irep_idt > function_parameter_to_associated_array_size
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...
std::map< irep_idt, irep_idt > function_argument_to_associated_array_size
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
std::vector< std::set< irep_idt > > function_arguments_to_treat_equal
const symbolt & lookup_function_to_call()
Return a reference to the entry function or throw if it doesn't exist.
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.
void add_harness_function_to_goto_model(code_blockt function_body)
Update the goto-model with the new harness function.
std::unique_ptr< recursive_initializationt > recursive_initialization
void generate_nondet_globals(code_blockt &function_body)
Iterate over the symbol table and generate initialisation code for globals into the function body.
ui_message_handlert * message_handler
recursive_initialization_configt recursive_initialization_config
void generate_initialisation_code_for(code_blockt &block, const exprt &lhs)
Generate initialisation code for one lvalue inside block.
std::set< irep_idt > function_parameters_to_treat_as_cstrings
std::vector< std::set< irep_idt > > function_parameters_to_treat_equal
std::set< irep_idt > function_arguments_to_treat_as_cstrings
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...
void ensure_harness_does_not_already_exist()
Throw if the harness function already exists in the symbol table.
std::set< irep_idt > pointers_to_treat_as_cstrings
std::vector< std::set< irep_idt > > pointers_to_treat_equal
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
std::set< irep_idt > variables_that_hold_array_sizes
std::set< irep_idt > pointers_to_treat_as_arrays
std::unordered_set< irep_idt > potential_null_function_pointers
typet remove_const(typet type)
Remove const qualifier from type (if any).