Go to the documentation of this file.
96 options.
set_option(
"unwinding-assertions",
false);
99 "unwinding-assertions",
108 log.
error() <<
"--partial-loops and --unwinding-assertions"
180 impact_modet::FORWARD :
182 impact_modet::BACKWARD :
237 const auto cover_config =
268 " goto_diff [-?] [-h] [--help] show help\n"
269 " goto_diff old new goto binaries to be compared\n"
274 " --syntactic do syntactic diff (default)\n"
275 " -u | --unified output unified diff\n"
276 " --change-impact | \n"
277 " --forward-impact |\n"
279 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
280 " --compact-output output dependencies in compact mode\n"
282 "Program instrumentation options:\n"
287 " --version show version and exit\n"
288 " --json-ui use JSON-formatted output\n"
Coverage Instrumentation.
#define HELP_SHOW_GOTO_FUNCTIONS
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
int doit() override
invoke main modules
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output(std::ostream &os) const
ui_message_handlert ui_message_handler
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
#define GOTO_DIFF_OPTIONS
virtual bool isset(char option) const
void help() override
display command line help
mstreamt & status() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
void set_option(const std::string &option, const bool value)
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
struct configt::ansi_ct ansi_c
void label_properties(goto_modelt &goto_model)
virtual uit get_ui() const
virtual void usage_error()
Unified diff (using LCSS) of goto functions.
Set the properties to check.
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
void register_languages() override
virtual void output_functions() const
Output diff result.
const char * CBMC_VERSION
Initialize a Goto Program.
std::string banner_string(const std::string &front_end, const std::string &version)
std::string get_value(char option) const
#define HELP_SHOW_PROPERTIES
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
GOTO-DIFF Command Line Option Processing.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
goto_diff_parse_optionst(int argc, const char **argv)
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
bool set(const cmdlinet &cmdline)
Document and give macros for the exit codes of CPROVER binaries.
bool get_bool_option(const std::string &option) const
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Data and control-dependencies of syntactic diff.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
void get_command_line_options(optionst &options)
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
symbol_tablet symbol_table
Symbol table.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)