55 languages2(cmdline, ui_message_handler)
62 const std::string &extra_options):
66 languages2(cmdline, ui_message_handler)
163 options.
set_option(
"div-by-zero-check",
true);
165 options.
set_option(
"div-by-zero-check",
false);
169 options.
set_option(
"signed-overflow-check",
true);
171 options.
set_option(
"signed-overflow-check",
false);
175 options.
set_option(
"unsigned-overflow-check",
true);
177 options.
set_option(
"unsigned-overflow-check",
false);
181 options.
set_option(
"float-overflow-check",
true);
183 options.
set_option(
"float-overflow-check",
false);
199 options.
set_option(
"memory-leak-check",
true);
201 options.
set_option(
"memory-leak-check",
false);
221 options.
set_option(
"unwinding-assertions",
false);
224 "unwinding-assertions",
233 error() <<
"--partial-loops and --unwinding-assertions" 234 <<
" must not be given together" <<
eom;
260 <<
sizeof(
void *)*8 <<
"-bit " 266 error() <<
"Please provide two programs to compare" <<
eom;
272 int get_goto_program_ret=
274 if(get_goto_program_ret!=-1)
275 return get_goto_program_ret;
276 get_goto_program_ret=
278 if(get_goto_program_ret!=-1)
279 return get_goto_program_ret;
321 std::unique_ptr<goto_difft> goto_diff;
322 goto_diff = std::unique_ptr<goto_difft>(
359 std::string arg2(
"");
374 status() <<
"Generating GOTO Program" <<
eom;
409 status() <<
"Function Pointer Removal" <<
eom;
456 catch(
const std::string e)
467 catch(std::bad_alloc)
482 "* * GOTO_DIFF " CBMC_VERSION " - Copyright (C) 2016 * *\n" 483 "* * Daniel Kroening, Peter Schrammel * *\n" 484 "* * kroening@kroening.com * *\n" 488 " goto_diff [-?] [-h] [--help] show help\n" 489 " goto_diff old new goto binaries to be compared\n" 493 " --syntactic do syntactic diff (default)\n" 494 " -u | --unified output unified diff\n" 495 " --change-impact | \n" 496 " --forward-impact |\n" 498 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n" 499 " --compact-output output dependencies in compact mode\n" 502 " --version show version and exit\n" 503 " --json-ui use JSON-formatted output\n" virtual std::ostream & output_functions(std::ostream &out) const
symbol_tablet symbol_table
const std::list< std::string > & get_values(const std::string &option) const
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
struct configt::ansi_ct ansi_c
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Remove Indirect Function Calls.
unsigned unsafe_string2unsigned(const std::string &str, int base)
virtual int get_goto_program(const optionst &options, goto_diff_languagest &languages, goto_modelt &goto_model)
Data and control-dependencies of syntactic diff.
bool is_goto_binary(const std::string &filename)
Remove the 'complex' data type by compilation into structs.
#define GOTO_DIFF_OPTIONS
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
std::string get_value(char option) const
symbol_tablet symbol_table
static mstreamt & eom(mstreamt &m)
goto_diff_languagest languages2
virtual void help()
display command line help
Remove 'asm' statements by compiling into suitable standard code.
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Set the properties to check.
void compute_loop_numbers()
void set_ui(language_uit::uit _ui)
bool set(const cmdlinet &cmdline)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
virtual bool isset(char option) const
virtual int doit()
invoke main modules
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)
GOTO-DIFF Command Line Option Processing.
Unified diff (using LCSS) of goto functions.
void set_from_symbol_table(const symbol_tablet &)
static irep_idt this_operating_system()
message_handlert & get_message_handler()
Goto Programs with Functions.
void output(std::ostream &os) const
ui_message_handlert ui_message_handler
#define HELP_SHOW_GOTO_FUNCTIONS
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Remove the 'vector' data type by compilation into arrays.
void set_verbosity(unsigned _verbosity)
virtual void usage_error()
void set_option(const std::string &option, const bool value)
void add_failed_symbols(symbol_tablet &symbol_table)
static void remove_complex(typet &)
removes complex data type
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
goto_functionst 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)