Go to the documentation of this file.
66 ui_message_handler(cmdline, std::string(
"GOTO-DIFF ") +
CBMC_VERSION),
67 languages2(cmdline, ui_message_handler)
74 const std::string &extra_options)
77 ui_message_handler(cmdline, std::string(
"GOTO-DIFF ") +
CBMC_VERSION),
78 languages2(cmdline, ui_message_handler)
207 "unwinding-assertions",
216 error() <<
"--partial-loops and --unwinding-assertions"
217 <<
" must not be given together" <<
eom;
251 error() <<
"Please provide two programs to compare" <<
eom;
257 int get_goto_program_ret=
259 if(get_goto_program_ret!=-1)
260 return get_goto_program_ret;
261 get_goto_program_ret=
263 if(get_goto_program_ret!=-1)
264 return get_goto_program_ret;
351 std::string arg2(
"");
366 status() <<
"Generating GOTO Program" <<
eom;
403 status() <<
"Removal of function pointers and virtual functions" <<
eom;
419 status() <<
"Generic Property Instrumentation" <<
eom;
459 catch(
const std::string &e)
467 error() <<
"Numeric exception: " << e <<
eom;
471 catch(
const std::bad_alloc &)
487 "* * Copyright (C) 2016 * *\n"
488 "* * Daniel Kroening, Peter Schrammel * *\n"
489 "* * kroening@kroening.com * *\n"
493 " goto_diff [-?] [-h] [--help] show help\n"
494 " goto_diff old new goto binaries to be compared\n"
499 " --syntactic do syntactic diff (default)\n"
500 " -u | --unified output unified diff\n"
501 " --change-impact | \n"
502 " --forward-impact |\n"
504 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
505 " --compact-output output dependencies in compact mode\n"
507 "Program instrumentation options:\n"
509 " --cover CC create test-suite with coverage criterion CC\n"
511 " --version show version and exit\n"
512 " --json-ui use JSON-formatted output\n"
const char * CBMC_VERSION
#define HELP_SHOW_GOTO_FUNCTIONS
virtual bool process_goto_program(const optionst &options, goto_modelt &goto_model)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output(std::ostream &os) const
bool is_goto_binary(const std::string &filename)
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
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Read a goto binary from a file, but do not update config.
mstreamt & status() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
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)
struct configt::ansi_ct ansi_c
goto_diff_languagest languages2
void label_properties(goto_modelt &goto_model)
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
virtual void usage_error()
static void remove_vector(typet &)
removes vector data type
virtual int get_goto_program(const optionst &options, goto_diff_languagest &languages, goto_modelt &goto_model)
virtual void output_functions() const
Output diff result.
std::string banner_string(const std::string &front_end, const std::string &version)
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
virtual void help()
display command line help
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
std::string get_value(char option) const
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
#define HELP_SHOW_PROPERTIES
static irep_idt this_operating_system()
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
void compute_loop_numbers()
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
static void remove_complex(typet &)
removes complex data type
virtual int doit()
invoke main modules
static irep_idt this_architecture()
message_handlert & get_message_handler()
goto_functionst goto_functions
GOTO functions.
goto_diff_parse_optionst(int argc, const char **argv)
ui_message_handlert ui_message_handler
void instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler)
Applies instrumenters to given goto program.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
bool set(const cmdlinet &cmdline)
bool get_bool_option(const std::string &option) const
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
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...
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
virtual 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.
const std::list< std::string > & get_values(const std::string &option) const
symbol_tablet symbol_table
Symbol table.
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)