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 std::list< std::string > & get_values(const std::string &option) const
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)
struct configt::ansi_ct ansi_c
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Remove Indirect Function Calls.
Functions for replacing virtual function call with a static function calls in functions,...
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
void compute_loop_numbers()
virtual int get_goto_program(const optionst &options, goto_diff_languagest &languages, goto_modelt &goto_model)
Data and control-dependencies of syntactic diff.
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.
bool is_goto_binary(const std::string &filename)
Remove the 'complex' data type by compilation into structs.
#define GOTO_DIFF_OPTIONS
std::string get_value(char option) const
symbol_tablet symbol_table
Symbol table.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
goto_diff_languagest languages2
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
virtual void help()
display command line help
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
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_SUCCESS
Success indicates the required analysis has been performed without error.
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Set the properties to check.
bool set(const cmdlinet &cmdline)
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.
Perform Memory-mapped I/O instrumentation.
virtual bool isset(char option) const
#define HELP_SHOW_PROPERTIES
virtual int doit()
invoke main modules
virtual void output_functions() const
Output diff result.
bool get_bool_option(const std::string &option) const
Abstract interface to support a programming language.
virtual void get_command_line_options(optionst &options)
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 bool process_goto_program(const optionst &options, goto_modelt &goto_model)
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
GOTO-DIFF Command Line Option Processing.
std::string banner_string(const std::string &front_end, const std::string &version)
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.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
Unified diff (using LCSS) of goto functions.
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...
static irep_idt this_operating_system()
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
message_handlert & get_message_handler()
Goto Programs with Functions.
void output(std::ostream &os) const
ui_message_handlert ui_message_handler
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
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.
virtual void usage_error()
Coverage Instrumentation.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
void set_option(const std::string &option, const bool value)
static void remove_complex(typet &)
removes complex data type
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
goto_diff_parse_optionst(int argc, const char **argv)