Go to the documentation of this file.
57 auto read_goto_binary_result =
59 if(!read_goto_binary_result.has_value())
62 got_harness_config.in_file +
"'"};
64 auto goto_model = std::move(read_goto_binary_result.value());
71 if(goto_model.symbol_table.has_symbol(
72 got_harness_config.harness_function_name))
75 "harness function `" +
76 id2string(got_harness_config.harness_function_name) +
83 auto harness_generator = factory.factory(
84 got_harness_config.harness_type, factory_options, goto_model);
87 harness_generator->generate(
88 goto_model, got_harness_config.harness_function_name);
95 got_harness_config.out_file +
"'"};
110 <<
"Usage: Purpose:\n"
112 <<
" goto-harness [-?] [-h] [--help] show help\n"
113 <<
" goto-harness --version show version\n"
114 <<
" goto-harness <in> <out> --harness-function-name <name> --harness-type "
115 "<harness-type> [harness options]\n"
117 <<
"<in> <out> goto binaries to read from / write to\n"
118 <<
"--harness-function-name the name of the harness function to "
120 <<
"--harness-type one of the harness types listed below\n"
147 "need to specify both input and output goto binary file names (may be "
149 "<in goto binary> <out goto binary>"};
160 goto_harness_config.harness_type =
167 "required option not set",
170 goto_harness_config.harness_function_name = {
173 return goto_harness_config;
180 return util_make_unique<function_call_harness_generatort>(
184 factory.register_generator(
"initialise-with-memory-snapshot", [
this]() {
185 return util_make_unique<memory_snapshot_harness_generatort>(
195 auto const common_options =
196 std::set<std::string>{
"version",
204 if(common_options.find(option) == common_options.end())
210 return factory_options;
const char * CBMC_VERSION
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
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
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
#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[])
void register_generator(std::string generator_name, build_generatort build_generator)
register a new goto-harness generator with the given name.
goto_harness_generator_factoryt::generator_optionst collect_generate_factory_options()
Gather all the options that are not handled by handle_common_options().
std::map< std::string, std::list< std::string > > generator_optionst
#define GOTO_HARNESS_OPTIONS
std::string banner_string(const std::string &front_end, const std::string &version)
const std::string & id2string(const irep_idt &d)
std::string get_value(char option) const
Thrown when some external system fails unexpectedly.
helper to select harness type by name.
void set_from_symbol_table(const symbol_tablet &)
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.
bool set(const cmdlinet &cmdline)
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 ...
const std::list< std::string > & get_values(const std::string &option) const
#define FUNCTION_HARNESS_GENERATOR_HELP
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".