68 languages2(cmdline, ui_message_handler)
75 const std::string &extra_options)
79 languages2(cmdline, ui_message_handler)
147 options.
set_option(
"div-by-zero-check",
true);
149 options.
set_option(
"div-by-zero-check",
false);
153 options.
set_option(
"signed-overflow-check",
true);
155 options.
set_option(
"signed-overflow-check",
false);
159 options.
set_option(
"unsigned-overflow-check",
true);
161 options.
set_option(
"unsigned-overflow-check",
false);
165 options.
set_option(
"float-overflow-check",
true);
167 options.
set_option(
"float-overflow-check",
false);
183 options.
set_option(
"memory-leak-check",
true);
185 options.
set_option(
"memory-leak-check",
false);
205 options.
set_option(
"unwinding-assertions",
false);
208 "unwinding-assertions",
217 error() <<
"--partial-loops and --unwinding-assertions" 218 <<
" must not be given together" <<
eom;
252 error() <<
"Please provide two programs to compare" <<
eom;
258 int get_goto_program_ret=
260 if(get_goto_program_ret!=-1)
261 return get_goto_program_ret;
262 get_goto_program_ret=
264 if(get_goto_program_ret!=-1)
265 return get_goto_program_ret;
353 std::string arg2(
"");
368 status() <<
"Generating GOTO Program" <<
eom;
405 status() <<
"Removal of function pointers and virtual functions" <<
eom;
421 status() <<
"Generic Property Instrumentation" <<
eom;
461 catch(
const std::string &e)
469 error() <<
"Numeric exception: " << e <<
eom;
473 catch(
const std::bad_alloc &)
489 "* * Copyright (C) 2016 * *\n" 490 "* * Daniel Kroening, Peter Schrammel * *\n" 491 "* * kroening@kroening.com * *\n" 495 " goto_diff [-?] [-h] [--help] show help\n" 496 " goto_diff old new goto binaries to be compared\n" 501 " --syntactic do syntactic diff (default)\n" 502 " -u | --unified output unified diff\n" 503 " --change-impact | \n" 504 " --forward-impact |\n" 506 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n" 507 " --compact-output output dependencies in compact mode\n" 509 "Program instrumentation options:\n" 511 " --cover CC create test-suite with coverage criterion CC\n" 513 " --version show version and exit\n" 514 " --json-ui use JSON-formatted output\n" void set_ui(ui_message_handlert::uit _ui)
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.
Remove Virtual Function (Method) Calls.
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.
static mstreamt & eom(mstreamt &m)
#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 into suitable standard code.
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)
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)
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)
removes assembler
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()
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
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)