68 languages2(cmdline, ui_message_handler)
75 const std::string &extra_options)
79 languages2(cmdline, ui_message_handler)
129 options.
set_option(
"div-by-zero-check",
true);
131 options.
set_option(
"div-by-zero-check",
false);
135 options.
set_option(
"signed-overflow-check",
true);
137 options.
set_option(
"signed-overflow-check",
false);
141 options.
set_option(
"unsigned-overflow-check",
true);
143 options.
set_option(
"unsigned-overflow-check",
false);
147 options.
set_option(
"float-overflow-check",
true);
149 options.
set_option(
"float-overflow-check",
false);
165 options.
set_option(
"memory-leak-check",
true);
167 options.
set_option(
"memory-leak-check",
false);
215 error() <<
"Please provide two programs to compare" <<
eom;
222 if(get_goto_program_ret != -1)
223 return get_goto_program_ret;
225 if(get_goto_program_ret != -1)
226 return get_goto_program_ret;
262 goto_model1, goto_model2, impact_mode,
cmdline.
isset(
"compact-output"));
310 std::string arg2(
"");
323 status() <<
"Generating GOTO Program" <<
eom;
347 status() <<
"Removal of function pointers and virtual functions" <<
eom;
370 status() <<
"Generic Property Instrumentation" <<
eom;
411 catch(
const std::string &e)
419 error() <<
"Numeric exception: " << e <<
eom;
423 catch(
const std::bad_alloc &)
439 "* * Copyright (C) 2016-2018 * *\n" 440 "* * Daniel Kroening, Peter Schrammel * *\n" 441 "* * kroening@kroening.com * *\n" 445 " jdiff [-?] [-h] [--help] show help\n" 446 " jdiff old new jars to be compared\n" 451 " --syntactic do syntactic diff (default)\n" 452 " -u | --unified output unified diff\n" 453 " --change-impact | \n" 454 " --forward-impact |\n" 456 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n" 457 " --compact-output output dependencies in compact mode\n" 459 "Program instrumentation options:\n" 461 " --cover CC create test-suite with coverage criterion CC\n" 462 "Java Bytecode frontend options:\n" 465 " --version show version and exit\n" 466 " --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 show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Remove function exceptional returns.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Remove Instance-of Operators.
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()
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.
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.
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 remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Syntactic GOTO-DIFF for Java.
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.
jdiff_languagest languages2
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.
ui_message_handlert ui_message_handler
virtual bool isset(char option) const
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
#define HELP_SHOW_PROPERTIES
virtual bool process_goto_program(const optionst &options, goto_modelt &goto_model)
virtual void output_functions() const
Output diff result.
virtual void set(const std::string &option)
Abstract interface to support a programming language.
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)
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.
virtual int doit()
invoke main modules
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
virtual int get_goto_program(const optionst &options, jdiff_languagest &languages, goto_modelt &goto_model)
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
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
virtual void get_command_line_options(optionst &options)
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)
JDIFF Command Line Option Processing.
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)
jdiff_parse_optionst(int argc, const char **argv)
goto_functionst goto_functions
GOTO functions.
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
virtual void help()
display command line help