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)
112 if(
p_impl->recursive_initialization_config.handle_option(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)
133 for(
auto const ¶m_cluster :
split_string(value,
';'))
135 std::set<irep_idt> equal_param_set;
136 for(
auto const ¶m_id :
split_string(param_cluster,
','))
138 equal_param_set.insert(param_id);
140 p_impl->function_parameters_to_treat_equal.push_back(equal_param_set);
146 for(
auto const &array_size_pair : values)
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(
163 "can not have two associated array sizes for one array",
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 "
180 p_impl->function_parameters_to_treat_as_cstrings.insert(
181 values.begin(), values.end());
185 p_impl->recursive_initialization_config.arguments_may_be_equal =
true;
193 p_impl->recursive_initialization_config
194 .potential_null_function_pointers,
195 p_impl->recursive_initialization_config.potential_null_function_pointers
197 [](
const std::string &opt) ->
irep_idt { return irep_idt{opt}; });
205 p_impl->recursive_initialization_config
206 .potential_null_function_pointers,
207 p_impl->recursive_initialization_config.potential_null_function_pointers
209 [](
const std::string &opt) ->
irep_idt { return irep_idt{opt}; });
214 "function harness generator cannot handle this option",
"--" + option};
220 const irep_idt &harness_function_name)
222 p_impl->generate(goto_model, harness_function_name);
227 const irep_idt &harness_function_name)
280 auto globals = std::vector<symbol_exprt>{};
281 for(
const auto &symbol_table_entry : *symbol_table)
283 const auto &symbol = symbol_table_entry.second;
286 globals.push_back(symbol.symbol_expr());
289 for(
auto const &global : globals)
291 generate_initialisation_code_for(function_body, global);
300 recursive_initialization->initialize(
302 if(recursive_initialization->needs_freeing(lhs))
309 if(
p_impl->function == ID_empty_string)
311 "required parameter entry function not set",
314 p_impl->recursive_initialization_config.min_dynamic_array_size >
315 p_impl->recursive_initialization_config.max_dynamic_array_size)
318 "min dynamic array size cannot be greater than max dynamic array size",
323 const auto function_to_call_pointer =
325 if(function_to_call_pointer ==
nullptr)
329 "' does not exist in the symbol table",
334 for(
auto const &equal_cluster :
p_impl->function_parameters_to_treat_equal)
336 for(
auto const &pointer_id : equal_cluster)
338 std::string decorated_pointer_id =
340 bool is_a_param =
false;
342 for(
auto const &formal_param : ftype.parameters())
344 if(formal_param.get_identifier() == decorated_pointer_id)
347 if(formal_param.type().id() != ID_pointer)
350 id2string(pointer_id) +
" is not a pointer parameter",
353 if(common_type.
id() != ID_empty)
355 if(common_type != formal_param.type())
358 "pointer arguments of conflicting type",
363 common_type = formal_param.type();
369 id2string(pointer_id) +
" is not a parameter",
379 for(
const auto &nullable :
380 p_impl->recursive_initialization_config.potential_null_function_pointers)
382 const auto &function_pointer_symbol_pointer =
385 if(function_pointer_symbol_pointer ==
nullptr)
388 "nullable function pointer `" +
id2string(nullable) +
389 "' not found in symbol table",
393 const auto &function_pointer_type =
394 ns.follow(function_pointer_symbol_pointer->type);
399 "`" +
id2string(nullable) +
"' is not a pointer",
407 "`" +
id2string(nullable) +
"' is not pointing to a function",
416 auto function_found = symbol_table->lookup(
function);
418 if(function_found ==
nullptr)
421 "function that should be harnessed is not found " +
id2string(
function),
425 return *function_found;
431 if(symbol_table->lookup(harness_function_name))
434 "harness function already exists in the symbol table",
445 symbolt harness_function_symbol{};
446 harness_function_symbol.
name = harness_function_symbol.base_name =
447 harness_function_symbol.pretty_name = harness_function_name;
449 harness_function_symbol.is_lvalue =
true;
452 harness_function_symbol.value = std::move(function_body);
454 symbol_table->insert(harness_function_symbol);
456 auto const &generated_harness =
457 symbol_table->lookup_ref(harness_function_name);
458 goto_functions->function_map[harness_function_name].type =
460 goto_convert(*symbol_table, *goto_functions, *message_handler);
469 const auto ¶meters = function_type.parameters();
477 std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
478 for(
const auto ¶meter : parameters)
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);
487 for(
const auto &pair : parameter_name_to_argument_name)
489 auto const ¶meter_name = pair.first;
490 auto const &argument_name = pair.second;
491 if(function_parameters_to_treat_as_arrays.count(parameter_name) != 0)
493 function_arguments_to_treat_as_arrays.insert(argument_name);
496 if(function_parameters_to_treat_as_cstrings.count(parameter_name) != 0)
498 function_arguments_to_treat_as_cstrings.insert(argument_name);
501 auto it = function_parameter_to_associated_array_size.find(parameter_name);
502 if(it != function_parameter_to_associated_array_size.end())
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);
508 associated_array_size_argument == parameter_name_to_argument_name.end())
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 \"" +
518 function_argument_to_associated_array_size.insert(
519 {argument_name, associated_array_size_argument->second});
524 for(
auto const &equal_cluster : function_parameters_to_treat_equal)
526 std::set<irep_idt> cluster_argument_names;
527 for(
auto const ¶meter_name : equal_cluster)
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]);
535 function_arguments_to_treat_equal.push_back(cluster_argument_names);
538 allocate_objects.declare_created_symbols(function_body);
547 for(
auto const &argument : arguments)
549 generate_initialisation_code_for(function_body, argument);
550 if(recursive_initialization->needs_freeing(argument))
554 std::move(arguments)};
557 function_body.
add(std::move(function_call));
563 std::unordered_set<irep_idt> nullables;
564 for(
const auto &nullable :
565 recursive_initialization_config.potential_null_function_pointers)
567 const auto &nullable_name =
id2string(nullable);
568 const auto &function_prefix =
id2string(
function) +
"::";
569 if(
has_prefix(nullable_name, function_prefix))
572 "__goto_harness::" + nullable_name.substr(function_prefix.size()));
576 nullables.insert(nullable_name);