Go to the documentation of this file.
91 const std::string &extra_options)
107 options.
set_option(
"built-in-assertions",
true);
116 options.
set_option(
"show-goto-symex-steps",
false);
141 "max-field-sensitivity-array-size",
150 <<
"--no-array-field-sensitivity and --max-field-sensitivity-array-size"
154 options.
set_option(
"no-array-field-sensitivity",
true);
206 if(
cmdline.
isset(
"symex-complexity-failed-child-loops-limit"))
209 "symex-complexity-failed-child-loops-limit",
231 "self-loops-to-assumptions",
239 options.
set_option(
"java-unwind-enum-static",
true);
251 options.
set_option(
"unwinding-assertions",
true);
261 log.
error() <<
"--partial-loops and --unwinding-assertions "
292 options.
set_option(
"refine-arithmetic",
true);
299 options.
set_option(
"refine-arithmetic",
true);
308 "cannot use --string-printable with --no-refine-strings",
309 "--string-printable");
315 "cannot use --string-input-value with --no-refine-strings",
316 "--string-input-value");
324 "cannot use --max-nondet-string-length with --no-refine-strings",
325 "--max-nondet-string-length");
330 "max-node-refinement",
347 bool solver_set=
false;
351 options.
set_option(
"boolector",
true), solver_set=
true;
357 options.
set_option(
"mathsat",
true), solver_set=
true;
363 options.
set_option(
"cvc4",
true), solver_set=
true;
369 options.
set_option(
"yices",
true), solver_set=
true;
375 options.
set_option(
"z3",
true), solver_set=
true;
397 options.
set_option(
"sat-preprocessor",
false);
415 "symex-coverage-report",
420 options.
set_option(
"validate-ssa-equation",
true);
425 options.
set_option(
"validate-goto-model",
true);
435 options.
set_option(
"symex-driven-lazy-loading",
true);
436 for(
const char *opt :
439 "reachability-slice",
440 "reachability-slice-fb" })
444 throw std::string(
"Option ") + opt +
445 " can't be used with --symex-driven-lazy-loading";
456 options.
set_option(
"allow-pointer-unsoundness",
true);
459 options.
set_option(
"show-goto-symex-steps",
true);
494 debug_stream <<
"\nOptions: \n";
495 options.
output(debug_stream);
518 log.
error() <<
"Please give exactly one class name, "
519 <<
"and/or use -jar jarfile or --gb goto-binary"
528 std::replace(main_class.begin(), main_class.end(),
'/',
'.');
568 std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
570 if(get_goto_program_ret != -1)
571 return get_goto_program_ret;
624 std::unique_ptr<goto_verifiert> verifier =
nullptr;
630 util_make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
682 const resultt result = (*verifier)();
688 std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
691 if(options.
is_set(
"context-include") || options.
is_set(
"context-exclude"))
698 util_make_unique<class_hierarchyt>(lazy_goto_model.
symbol_table);
723 std::move(lazy_goto_model));
724 if(goto_model_ptr ==
nullptr)
761 util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
778 bool using_symex_driven_loading =
783 function.get_function_id(),
791 auto function_is_stub = [&symbol_table, &model](
const irep_idt &id) {
803 if(using_symex_driven_loading)
811 function.get_function_id(),
820 function.get_function_id(),
function.get_goto_function(), ns, options);
824 function.get_function_id(),
836 for(
const irep_idt &new_symbol_name : new_symbols)
839 symbol_table.
lookup_ref(new_symbol_name), symbol_table);
846 if(using_symex_driven_loading)
851 goto_function.body.update();
852 function.compute_location_numbers();
853 goto_function.body.compute_loop_numbers();
910 log.
status() <<
"Running GOTO functions transformation passes"
913 bool using_symex_driven_loading =
918 if(using_symex_driven_loading)
931 log.
status() <<
"Adding nondeterministic initialization "
932 "of static/global variables"
962 log.
error() <<
"--reachability-slice and --reachability-slice-fb "
967 log.
status() <<
"Performing a forwards-backwards reachability slice"
1011 bool body_available)
1056 " jbmc [-?] [-h] [--help] show help\n"
1069 "Analysis options:\n"
1071 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n"
1072 " --property id only check one specific property\n"
1073 " --stop-on-fail stop analysis once a failed property is detected\n"
1074 " --trace give a counterexample trace for failed properties\n"
1077 "Program representations:\n"
1078 " --show-parse-tree show parse tree\n"
1079 " --show-symbol-table show loaded symbol table\n"
1080 " --list-symbols list symbols with type information\n"
1082 " --drop-unused-functions drop functions trivially unreachable\n"
1083 " from main function\n"
1086 "Program instrumentation options:\n"
1087 " --no-assertions ignore user assertions\n"
1088 " --no-assumptions ignore user assumptions\n"
1089 " --error-label label check that label is unreachable\n"
1090 " --mm MM memory consistency model for concurrent programs\n"
1092 " --full-slice run full slicer (experimental)\n"
1094 "Java Bytecode frontend options:\n"
1098 " --java-threading enable java multi-threading support (experimental)\n"
1099 " --java-unwind-enum-static unwind loops in static initialization of enums\n"
1101 " --symex-driven-lazy-loading only load functions when first entered by symbolic\n"
1102 " execution. Note that --show-symbol-table,\n"
1103 " --show-goto-functions/properties output\n"
1104 " will be restricted to loaded methods in this case,\n"
1105 " and only output after the symex phase.\n"
1107 "Semantic transformations:\n"
1109 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1114 "Backend options:\n"
1115 " --object-bits n number of bits used for object addresses\n"
1116 " --dimacs generate CNF in DIMACS format\n"
1117 " --beautify beautify the counterexample (greedy heuristic)\n"
1118 " --localize-faults localize faults (experimental)\n"
1119 " --smt1 use default SMT1 solver (obsolete)\n"
1120 " --smt2 use default SMT2 solver (Z3)\n"
1121 " --boolector use Boolector\n"
1122 " --mathsat use MathSAT\n"
1123 " --cvc4 use CVC4\n"
1124 " --yices use Yices\n"
1126 " --refine use refinement procedure (experimental)\n"
1128 " --outfile filename output formula to given file\n"
1129 " --arrays-uf-never never turn arrays into uninterpreted functions\n"
1130 " --arrays-uf-always always turn arrays into uninterpreted functions\n"
1133 " --version show version and exit\n"
1139 " --verbosity # verbosity level\n"
#define UNREACHABLE
This should be used to mark dead code.
Convert side_effect_expr_nondett expressions using java_object_factory.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define HELP_REACHABILITY_SLICER
#define HELP_SHOW_GOTO_FUNCTIONS
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
virtual void show_parse(std::ostream &out)=0
std::string object_bits_info()
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output(std::ostream &out) const
Outputs the options to out
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
void get_command_line_options(optionst &)
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.
resultt
The result of goto verifying.
virtual bool isset(char option) const
Stops when the first failing property is found.
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
#define CHECK_RETURN(CONDITION)
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
const std::string get_option(const std::string &option) const
mstreamt & status() const
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we've already loaded but is frozen in the sense t...
Unwind loops in static initializers.
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::unique_ptr< languaget > new_java_bytecode_language()
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Functions for replacing virtual function call with a static function calls in functions,...
#define HELP_SHOW_CLASS_HIERARCHY
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
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 show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Goto Verifier for Verifying all Properties.
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)
#define HELP_JAVA_GOTO_BINARY
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
java_object_factory_parameterst object_factory_params
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Nondeterministically initializes global scope variables, except for constants (such as string literal...
Java simple opaque stub generation.
Goto Verifier for stopping at the first failing property and localizing the fault.
void label_properties(goto_modelt &goto_model)
Storage of symbolic execution paths to resume.
bool stub_objects_are_not_null
virtual void set_language_options(const optionst &)
Set language-specific options.
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
void set(const optionst &)
Assigns the parameters from given options.
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...
#define HELP_JAVA_TRACE_VALIDATION
void parse_path_strategy_options(const cmdlinet &cmdline, optionst &options, message_handlert &message_handler)
add paths and exploration-strategy option, suitable to be invoked from front-ends.
#define HELP_JSON_INTERFACE
virtual uit get_ui() const
virtual void usage_error()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Set the properties to check.
static lazy_goto_modelt from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler)
Create a lazy_goto_modelt from a object that defines function/module pass handlers.
json_objectt to_json() const
Returns the options as JSON key value pairs.
void convert_nondet(const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &user_object_factory_parameters, const irep_idt &mode)
For each instruction in the goto program, checks if it is an assignment from nondet and replaces it w...
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
virtual int doit() override
invoke main modules
const char * CBMC_VERSION
void parse_java_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the java object factory parameters from a given command line.
irep_idt mode
Language mode.
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Goto verifier for verifying all properties that stores traces.
bool can_generate_function_body(const irep_idt &name)
#define HELP_STRING_REFINEMENT
std::string banner_string(const std::string &front_end, const std::string &version)
const std::string & id2string(const irep_idt &d)
A GOTO model that produces function bodies on demand.
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
The symbol table base class interface.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Goto Checker using Single Path Symbolic Execution for Java.
prefix_filtert get_context(const optionst &options)
std::unique_ptr< class_hierarchyt > class_hierarchy
#define INITIALIZE_FUNCTION
std::string get_value(char option) const
Abstract interface to support a programming language.
virtual void set_message_handler(message_handlert &_message_handler)
std::unordered_set< irep_idt > changesett
#define HELP_SHOW_PROPERTIES
#define HELP_JAVA_CLASS_NAME
static irep_idt this_operating_system()
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
A goto function, consisting of function type (see type), function body (see body),...
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
void remove_java_new(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
Goto verifier for verifying all properties that stores traces and localizes faults.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
#define HELP_JAVA_METHOD_NAME
virtual void report()=0
Report results.
Replace function returns by assignments to global variables.
Remove function exceptional returns.
Remove Instance-of Operators.
::goto_functiont goto_functiont
static irep_idt this_architecture()
virtual void help() override
display command line help
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
exprt value
Initial value of symbol.
void java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
int result_to_exit_code(resultt result)
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
JBMC Command Line Option Processing.
goto_functionst goto_functions
GOTO functions.
Goto Verifier for stopping at the first failing property.
bool set(const cmdlinet &cmdline)
#define HELP_JAVA_CLASSPATH
Document and give macros for the exit codes of CPROVER binaries.
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
bool get_bool_option(const std::string &option) const
void add_failed_symbol_if_needed(const symbolt &symbol, symbol_table_baset &symbol_table)
Create a failed-dereference symbol for the given base symbol if it is pointer-typed,...
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
std::unique_ptr< languaget > new_ansi_c_language()
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
struct configt::javat java
std::string show_path_strategies()
suitable for displaying as a front-end help message
static void replace_java_nondet(goto_programt &goto_program)
Checks each instruction in the goto program to see whether it is a method returning nondet.
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
static void set_default_options(optionst &)
Set the options that have default values.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Abstract interface to eager or lazy GOTO models.
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Remove Java New Operators.
Goto Checker using Bounded Model Checking for Java.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
xmlt to_xml() const
Returns the options in XML format.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
const changesett & get_inserted() const
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
jbmc_parse_optionst(int argc, const char **argv)
Goto Programs with Functions.
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
#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.
Goto Checker using Single Path Symbolic Execution for Java.
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const std::list< std::string > & get_values(const std::string &option) const
Goto Checker using Bounded Model Checking for Java.
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
virtual const symbol_tablet & get_symbol_table() const override
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
#define HELP_XML_INTERFACE
Replace Java Nondet expressions.
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.