15#include <unordered_set>
35std::unordered_set<irep_idt>
38 auto symbols = std::unordered_set<irep_idt>{};
42 std::inserter(symbols, symbols.end()),
44 return key_value_pair.first;
57 if(symbol.is_function())
62 if(symbol.is_file_local)
67 else if(!symbol.is_type && symbol.is_file_local)
74 else if(!symbol.is_type && symbol.is_static_lifetime)
80 symbol.is_extern =
true;
131 if(goto_model.symbol_table.has_symbol(
135 "harness function `" +
155 goto_model.goto_functions,
180 <<
"Usage: Purpose:\n"
182 <<
" goto-harness [-?] [-h] [--help] show help\n"
183 <<
" goto-harness --version show version\n"
184 <<
" goto-harness <in> <out> --harness-function-name <name> --harness-type "
185 "<harness-type> [harness options]\n"
187 <<
"<in> goto binary to read from\n"
188 <<
"<out> file to write the harness to\n"
189 <<
" the harness is printed as C code, if <out> "
191 " else a goto binary including the harness is "
193 <<
"--harness-function-name the name of the harness function to "
195 <<
"--harness-type one of the harness types listed below\n"
222 "need to specify both input and output file names (may be "
224 "<in goto binary> <output C file or goto binary>"};
242 "required option not set",
259 factory.register_generator(
"initialise-with-memory-snapshot", [
this]() {
271 std::set<std::string>{
"version",
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::string get_value(char option) const
virtual bool isset(char option) const
option_namest option_names() const
Pseudo-object that can be used to iterate over options in this cmdlinet (should not outlive this)
const std::list< std::string > & get_values(const std::string &option) const
void set_from_symbol_table(const symbol_tablet &)
bool set(const cmdlinet &cmdline)
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
helper to select harness type by name.
std::map< std::string, std::list< std::string > > generator_optionst
void register_generator(std::string generator_name, build_generatort build_generator)
register a new goto-harness generator with the given name.
goto_harness_configt handle_common_options()
Handle command line arguments that are common to all harness generators.
goto_harness_parse_optionst(int argc, const char *argv[])
goto_harness_generator_factoryt make_factory()
Setup the generator factory.
goto_harness_generator_factoryt::generator_optionst collect_generate_factory_options()
Gather all the options that are not handled by handle_common_options().
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
message_handlert & get_message_handler()
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
ui_message_handlert ui_message_handler
virtual iteratort begin() override
virtual iteratort end() override
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)
Dump C from Goto Program.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
#define FUNCTION_HARNESS_GENERATOR_HELP
#define GOTO_HARNESS_GENERATOR_TYPE_OPT
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
std::unordered_set< irep_idt > get_symbol_names_from_goto_model(const goto_modelt &goto_model)
static void filter_goto_model(goto_modelt &goto_model_with_harness, const std::unordered_set< irep_idt > &goto_model_without_harness_symbols)
#define GOTO_HARNESS_OPTIONS
const std::string & id2string(const irep_idt &d)
#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
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 CHECK_RETURN(CONDITION)
bool has_suffix(const std::string &s, const std::string &suffix)
const char * CBMC_VERSION
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.