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)
757 util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
774 bool using_symex_driven_loading =
779 function.get_function_id(),
787 auto function_is_stub = [&symbol_table, &model](
const irep_idt &id) {
799 if(using_symex_driven_loading)
807 function.get_function_id(),
816 function.get_function_id(),
function.get_goto_function(), ns, options);
820 function.get_function_id(),
832 for(
const irep_idt &new_symbol_name : new_symbols)
835 symbol_table.
lookup_ref(new_symbol_name), symbol_table);
842 if(using_symex_driven_loading)
847 goto_function.body.update();
848 function.compute_location_numbers();
849 goto_function.body.compute_loop_numbers();
906 log.
status() <<
"Running GOTO functions transformation passes"
909 bool using_symex_driven_loading =
914 if(using_symex_driven_loading)
927 log.
status() <<
"Adding nondeterministic initialization "
928 "of static/global variables"
958 log.
error() <<
"--reachability-slice and --reachability-slice-fb "
963 log.
status() <<
"Performing a forwards-backwards reachability slice"
1007 bool body_available)
1052 " jbmc [-?] [-h] [--help] show help\n"
1065 "Analysis options:\n"
1067 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n"
1068 " --property id only check one specific property\n"
1069 " --stop-on-fail stop analysis once a failed property is detected\n"
1070 " --trace give a counterexample trace for failed properties\n"
1073 "Program representations:\n"
1074 " --show-parse-tree show parse tree\n"
1075 " --show-symbol-table show loaded symbol table\n"
1076 " --list-symbols list symbols with type information\n"
1078 " --drop-unused-functions drop functions trivially unreachable\n"
1079 " from main function\n"
1082 "Program instrumentation options:\n"
1083 " --no-assertions ignore user assertions\n"
1084 " --no-assumptions ignore user assumptions\n"
1085 " --error-label label check that label is unreachable\n"
1086 " --mm MM memory consistency model for concurrent programs\n"
1088 " --full-slice run full slicer (experimental)\n"
1090 "Java Bytecode frontend options:\n"
1094 " --java-threading enable java multi-threading support (experimental)\n"
1095 " --java-unwind-enum-static unwind loops in static initialization of enums\n"
1097 " --symex-driven-lazy-loading only load functions when first entered by symbolic\n"
1098 " execution. Note that --show-symbol-table,\n"
1099 " --show-goto-functions/properties output\n"
1100 " will be restricted to loaded methods in this case,\n"
1101 " and only output after the symex phase.\n"
1103 "Semantic transformations:\n"
1105 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1110 "Backend options:\n"
1111 " --object-bits n number of bits used for object addresses\n"
1112 " --dimacs generate CNF in DIMACS format\n"
1113 " --beautify beautify the counterexample (greedy heuristic)\n"
1114 " --localize-faults localize faults (experimental)\n"
1115 " --smt1 use default SMT1 solver (obsolete)\n"
1116 " --smt2 use default SMT2 solver (Z3)\n"
1117 " --boolector use Boolector\n"
1118 " --mathsat use MathSAT\n"
1119 " --cvc4 use CVC4\n"
1120 " --yices use Yices\n"
1122 " --refine use refinement procedure (experimental)\n"
1124 " --outfile filename output formula to given file\n"
1125 " --arrays-uf-never never turn arrays into uninterpreted functions\n"
1126 " --arrays-uf-always always turn arrays into uninterpreted functions\n"
1129 " --version show version and exit\n"
1135 " --verbosity # verbosity level\n"
const char * CBMC_VERSION
#define UNREACHABLE
This should be used to mark dead code.
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...
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.
#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)
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)
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)
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
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)
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)
prefix_filtert get_context(const optionst &options)
std::unique_ptr< class_hierarchyt > class_hierarchy
#define INITIALIZE_FUNCTION
std::string get_value(char option) const
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.
#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.
::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...
goto_functionst goto_functions
GOTO functions.
bool set(const cmdlinet &cmdline)
#define HELP_JAVA_CLASSPATH
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...
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)
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.
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
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/removed.
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
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.