Go to the documentation of this file.
15 #include <unordered_set>
36 std::unordered_set<irep_idt>
39 auto symbols = std::unordered_set<irep_idt>{};
43 std::inserter(symbols, symbols.end()),
44 [](
const std::pair<const irep_idt, symbolt> &key_value_pair) {
45 return key_value_pair.first;
52 const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
54 for(
auto const &symbol_id : goto_model_without_harness_symbols)
58 if(symbol.is_function())
62 goto_model_with_harness.
unload(symbol_id);
63 if(symbol.is_file_local)
68 else if(!symbol.is_type && symbol.is_file_local)
75 else if(!symbol.is_type && symbol.is_static_lifetime)
81 symbol.is_extern =
true;
113 auto read_goto_binary_result =
115 if(!read_goto_binary_result.has_value())
118 got_harness_config.in_file +
"'"};
120 auto goto_model = std::move(read_goto_binary_result.value());
121 auto const goto_model_without_harness_symbols =
129 if(goto_model.symbol_table.has_symbol(
130 got_harness_config.harness_function_name))
133 "harness function `" +
134 id2string(got_harness_config.harness_function_name) +
141 auto harness_generator = factory.factory(
142 got_harness_config.harness_type, factory_options, goto_model);
145 harness_generator->generate(
146 goto_model, got_harness_config.harness_function_name);
149 auto harness_out = std::ofstream{got_harness_config.out_file};
151 goto_model.goto_functions,
170 <<
"Usage: Purpose:\n"
172 <<
" goto-harness [-?] [-h] [--help] show help\n"
173 <<
" goto-harness --version show version\n"
174 <<
" goto-harness <in> <out> --harness-function-name <name> --harness-type "
175 "<harness-type> [harness options]\n"
177 <<
"<in> goto binaries to read from\n"
178 <<
"<out> C file to write the harness to\n"
179 <<
"--harness-function-name the name of the harness function to "
181 <<
"--harness-type one of the harness types listed below\n"
208 "need to specify both input and output goto binary file names (may be "
210 "<in goto binary> <out goto binary>"};
221 goto_harness_config.harness_type =
228 "required option not set",
231 goto_harness_config.harness_function_name = {
234 return goto_harness_config;
241 return util_make_unique<function_call_harness_generatort>(
245 factory.register_generator(
"initialise-with-memory-snapshot", [
this]() {
246 return util_make_unique<memory_snapshot_harness_generatort>(
256 auto const common_options =
257 std::set<std::string>{
"version",
265 if(common_options.find(option) == common_options.end())
271 return factory_options;
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
void unload(const irep_idt &name)
ui_message_handlert ui_message_handler
virtual bool isset(char option) const
#define GOTO_HARNESS_GENERATOR_TYPE_OPT
#define CHECK_RETURN(CONDITION)
mstreamt & status() const
#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
goto_harness_parse_optionst(int argc, const char *argv[])
static void filter_goto_model(goto_modelt &goto_model_with_harness, const std::unordered_set< irep_idt > &goto_model_without_harness_symbols)
void register_generator(std::string generator_name, build_generatort build_generator)
register a new goto-harness generator with the given name.
std::unordered_set< irep_idt > get_symbol_names_from_goto_model(const goto_modelt &goto_model)
goto_harness_generator_factoryt::generator_optionst collect_generate_factory_options()
Gather all the options that are not handled by handle_common_options().
virtual iteratort begin() override
std::map< std::string, std::list< std::string > > generator_optionst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const char * CBMC_VERSION
#define GOTO_HARNESS_OPTIONS
std::string banner_string(const std::string &front_end, const std::string &version)
virtual iteratort end() override
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
std::string get_value(char option) const
helper to select harness type by name.
void set_from_symbol_table(const symbol_tablet &)
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
option_namest option_names() const
Pseudo-object that can be used to iterate over options in this cmdlinet (should not outlive this)
goto_harness_generator_factoryt make_factory()
Setup the generator factory.
goto_harness_configt handle_common_options()
Handle command line arguments that are common to all harness generators.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool set(const cmdlinet &cmdline)
Document and give macros for the exit codes of CPROVER binaries.
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Dump C from Goto Program.
const std::list< std::string > & get_values(const std::string &option) const
symbol_tablet symbol_table
Symbol table.
#define FUNCTION_HARNESS_GENERATOR_HELP
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".