120 options.
set_option(
"unwinding-assertions",
false);
123 "unwinding-assertions",
132 log.
error() <<
"--partial-loops and --unwinding-assertions"
266 const auto cover_config =
297 " goto_diff [-?] [-h] [--help] show help\n"
298 " goto_diff old new goto binaries to be compared\n"
303 " --syntactic do syntactic diff (default)\n"
304 " -u | --unified output unified diff\n"
305 " --change-impact | \n"
306 " --forward-impact |\n"
308 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
309 " --compact-output output dependencies in compact mode\n"
311 "Program instrumentation options:\n"
316 " --version show version and exit\n"
317 " --json-ui use JSON-formatted output\n"
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 ...
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Data and control-dependencies of syntactic diff.
std::string get_value(char option) const
virtual bool isset(char option) const
bool set(const cmdlinet &cmdline)
static irep_idt this_architecture()
static irep_idt this_operating_system()
struct configt::ansi_ct ansi_c
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
virtual int doit()
invoke main modules
void register_languages()
goto_diff_parse_optionst(int argc, const char **argv)
void get_command_line_options(optionst &options)
virtual void help()
display command line help
virtual void output_functions() const
Output diff result.
symbol_tablet symbol_table
Symbol table.
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.
mstreamt & status() const
bool get_bool_option(const std::string &option) const
void set_option(const std::string &option, const bool value)
virtual void usage_error()
ui_message_handlert ui_message_handler
virtual uit get_ui() const
void output(std::ostream &os) const
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.
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 parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Coverage Instrumentation.
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Goto Programs with Functions.
GOTO-DIFF Command Line Option Processing.
#define GOTO_DIFF_OPTIONS
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
Abstract interface to support a programming language.
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.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Perform Memory-mapped I/O instrumentation.
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)
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...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Remove the 'complex' data type by compilation into structs.
Remove Indirect Function Calls.
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Remove the 'vector' data type by compilation into arrays.
Functions for replacing virtual function call with a static function calls in functions,...
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_PROPERTIES
Unified diff (using LCSS) of goto functions.
const char * CBMC_VERSION