Go to the documentation of this file.
117 options.
set_option(
"div-by-zero-check",
true);
119 options.
set_option(
"div-by-zero-check",
false);
123 options.
set_option(
"signed-overflow-check",
true);
125 options.
set_option(
"signed-overflow-check",
false);
129 options.
set_option(
"unsigned-overflow-check",
true);
131 options.
set_option(
"unsigned-overflow-check",
false);
135 options.
set_option(
"float-overflow-check",
true);
137 options.
set_option(
"float-overflow-check",
false);
153 options.
set_option(
"memory-leak-check",
true);
155 options.
set_option(
"memory-leak-check",
false);
246 goto_model1, goto_model2, impact_mode,
cmdline.
isset(
"compact-output"));
274 log.
status() <<
"Removing function pointers and virtual functions"
321 const auto cover_config =
354 " jdiff [-?] [-h] [--help] show help\n"
355 " jdiff old new jars to be compared\n"
360 " --syntactic do syntactic diff (default)\n"
361 " -u | --unified output unified diff\n"
362 " --change-impact | \n"
363 " --forward-impact |\n"
365 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
366 " --compact-output output dependencies in compact mode\n"
368 "Program instrumentation options:\n"
370 " --cover CC create test-suite with coverage criterion CC\n"
371 "Java Bytecode frontend options:\n"
374 " --version show version and exit\n"
375 " --json-ui use JSON-formatted output\n"
virtual int doit()
invoke main modules
Coverage Instrumentation.
#define HELP_SHOW_GOTO_FUNCTIONS
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output(std::ostream &os) const
void get_command_line_options(optionst &options)
Non-graph-based representation of the class hierarchy.
ui_message_handlert ui_message_handler
#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
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
mstreamt & status() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Functions for replacing virtual function call with a static function calls in functions,...
void remove_virtual_functions(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 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 goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
void set_option(const std::string &option, const bool value)
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
void label_properties(goto_modelt &goto_model)
virtual void set(const std::string &option, bool value=true)
Set option option to value, or true if the value is omitted.
void remove_instanceof(const irep_idt &function_identifier, 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...
virtual uit get_ui() const
virtual void usage_error()
static void remove_vector(typet &)
removes vector data type
Unified diff (using LCSS) of goto functions.
Remove the 'complex' data type by compilation into structs.
Set the properties to check.
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
virtual void output_functions() const
Output diff result.
const char * CBMC_VERSION
Initialize a Goto Program.
std::string banner_string(const std::string &front_end, const std::string &version)
Perform Memory-mapped I/O instrumentation.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
JDIFF Command Line Option Processing.
virtual void help()
display command line help
std::string get_value(char option) const
Syntactic GOTO-DIFF for Java.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Abstract interface to support a programming language.
#define HELP_SHOW_PROPERTIES
static irep_idt this_operating_system()
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
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,...
Remove the 'vector' data type by compilation into arrays.
static void remove_complex(typet &)
removes complex data type
Replace function returns by assignments to global variables.
Remove function exceptional returns.
Remove Instance-of Operators.
static irep_idt this_architecture()
goto_functionst goto_functions
GOTO functions.
void register_languages()
bool set(const cmdlinet &cmdline)
Document and give macros for the exit codes of CPROVER binaries.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
Data and control-dependencies of syntactic diff.
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Goto Programs with Functions.
#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.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
const std::list< std::string > & get_values(const std::string &option) const
Remove Indirect Function Calls.
symbol_tablet symbol_table
Symbol table.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".