Go to the documentation of this file.
68 ui_message_handler(cmdline, std::string(
"JDIFF ") +
CBMC_VERSION),
69 languages2(cmdline, ui_message_handler, &options)
76 const std::string &extra_options)
79 ui_message_handler(cmdline, std::string(
"JDIFF ") +
CBMC_VERSION),
80 languages2(cmdline, ui_message_handler, &options)
217 error() <<
"Please provide two programs to compare" <<
eom;
224 if(get_goto_program_ret != -1)
225 return get_goto_program_ret;
227 if(get_goto_program_ret != -1)
228 return get_goto_program_ret;
264 goto_model1, goto_model2, impact_mode,
cmdline.
isset(
"compact-output"));
311 std::string arg2(
"");
324 status() <<
"Generating GOTO Program" <<
eom;
348 status() <<
"Removing function pointers and virtual functions" <<
eom;
375 status() <<
"Generic Property Instrumentation" <<
eom;
416 catch(
const std::string &e)
424 error() <<
"Numeric exception: " << e <<
eom;
428 catch(
const std::bad_alloc &)
444 "* * Copyright (C) 2016-2018 * *\n"
445 "* * Daniel Kroening, Peter Schrammel * *\n"
446 "* * kroening@kroening.com * *\n"
450 " jdiff [-?] [-h] [--help] show help\n"
451 " jdiff old new jars to be compared\n"
456 " --syntactic do syntactic diff (default)\n"
457 " -u | --unified output unified diff\n"
458 " --change-impact | \n"
459 " --forward-impact |\n"
461 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
462 " --compact-output output dependencies in compact mode\n"
464 "Program instrumentation options:\n"
466 " --cover CC create test-suite with coverage criterion CC\n"
467 "Java Bytecode frontend options:\n"
470 " --version show version and exit\n"
471 " --json-ui use JSON-formatted output\n"
const char * CBMC_VERSION
virtual int doit()
invoke main modules
#define HELP_SHOW_GOTO_FUNCTIONS
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output(std::ostream &os) const
virtual void get_command_line_options(optionst &options)
bool is_goto_binary(const std::string &filename)
Non-graph-based representation of the class hierarchy.
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
virtual bool isset(char option) const
jdiff_languagest languages2
#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
virtual void set(const std::string &option)
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
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)
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 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)
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
virtual void help()
display command line help
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.
ui_message_handlert ui_message_handler
jdiff_parse_optionst(int argc, const char **argv)
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
static irep_idt this_architecture()
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
message_handlert & get_message_handler()
goto_functionst goto_functions
GOTO functions.
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.
bool set(const cmdlinet &cmdline)
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
virtual bool process_goto_program(const optionst &options, goto_modelt &goto_model)
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.
#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
virtual int get_goto_program(const optionst &options, jdiff_languagest &languages, goto_modelt &goto_model)
symbol_tablet symbol_table
Symbol table.