103 options.
set_option(
"built-in-assertions",
true);
112 options.
set_option(
"show-goto-symex-steps",
false);
138 "max-field-sensitivity-array-size",
147 <<
"--no-array-field-sensitivity and --max-field-sensitivity-array-size"
151 options.
set_option(
"no-array-field-sensitivity",
true);
203 if(
cmdline.
isset(
"symex-complexity-failed-child-loops-limit"))
206 "symex-complexity-failed-child-loops-limit",
228 "self-loops-to-assumptions",
236 options.
set_option(
"java-unwind-enum-static",
true);
248 options.
set_option(
"unwinding-assertions",
true);
258 log.
error() <<
"--partial-loops and --unwinding-assertions "
289 options.
set_option(
"refine-arithmetic",
true);
296 options.
set_option(
"refine-arithmetic",
true);
305 "cannot use --string-printable with --no-refine-strings",
306 "--string-printable");
312 "cannot use --string-input-value with --no-refine-strings",
313 "--string-input-value");
321 "cannot use --max-nondet-string-length with --no-refine-strings",
322 "--max-nondet-string-length");
327 "max-node-refinement",
394 options.
set_option(
"sat-preprocessor",
false);
412 "symex-coverage-report",
417 options.
set_option(
"validate-ssa-equation",
true);
422 options.
set_option(
"validate-goto-model",
true);
426 "symex-cache-dereferences",
cmdline.
isset(
"symex-cache-dereferences"));
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);
489 debug_stream <<
"\nOptions: \n";
490 options.output(debug_stream);
491 debug_stream << messaget::eom;
513 log.
error() <<
"Please give exactly one class name, "
514 <<
"and/or use -jar jarfile or --gb goto-binary"
523 std::replace(main_class.begin(), main_class.end(),
'/',
'.');
543 language->set_language_options(options);
554 language->show_parse(std::cout);
619 std::unique_ptr<goto_verifiert>
verifier =
nullptr;
677 const resultt result = (*verifier)();
686 if(options.
is_set(
"context-include") || options.
is_set(
"context-exclude"))
846 goto_function.body.update();
848 goto_function.body.compute_loop_numbers();
905 log.
status() <<
"Running GOTO functions transformation passes"
926 log.
status() <<
"Adding nondeterministic initialization "
927 "of static/global variables"
957 log.
error() <<
"--reachability-slice and --reachability-slice-fb "
962 log.
status() <<
"Performing a forwards-backwards reachability slice"
1006 bool body_available)
1051 " jbmc [-?] [-h] [--help] show help\n"
1064 "Analysis options:\n"
1066 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n"
1067 " --property id only check one specific property\n"
1068 " --trace give a counterexample trace for failed properties\n"
1069 " --stop-on-fail stop analysis once a failed property is detected\n"
1070 " (implies --trace)\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"
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 add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Goto Verifier for Verifying all Properties.
Goto verifier for verifying all properties that stores traces and localizes faults.
Goto verifier for verifying all properties that stores traces.
std::unique_ptr< languaget > new_ansi_c_language()
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
#define HELP_SHOW_CLASS_HIERARCHY
Abstract interface to eager or lazy GOTO models.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
bool set(const cmdlinet &cmdline)
std::string object_bits_info()
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
const irep_idt & get_function_id()
Get function id.
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
void compute_location_numbers()
Re-number our goto_function.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
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.
goto_functionst goto_functions
GOTO functions.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
void get_command_line_options(optionst &)
bool can_generate_function_body(const irep_idt &name)
std::unique_ptr< class_hierarchyt > class_hierarchy
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
virtual int doit() override
invoke main modules
virtual void help() override
display command line help
bool stub_objects_are_not_null
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
java_object_factory_parameterst object_factory_params
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
jbmc_parse_optionst(int argc, const char **argv)
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
static void set_default_options(optionst &)
Set the options that have default values.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const changesett & get_inserted() const
std::unordered_set< irep_idt > changesett
A GOTO model that produces function bodies on demand.
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...
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.
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.
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...
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
json_objectt to_json() const
Returns the options as JSON key value pairs.
bool get_bool_option(const std::string &option) const
void set_option(const std::string &option, const bool value)
const std::string get_option(const std::string &option) const
xmlt to_xml() const
Returns the options in XML format.
virtual void usage_error()
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
ui_message_handlert ui_message_handler
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
virtual uit get_ui() const
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...
Convert side_effect_expr_nondett expressions using java_object_factory.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void goto_check_java(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
#define PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options)
Goto Programs with Functions.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
const std::string & id2string(const irep_idt &d)
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
std::unique_ptr< languaget > new_java_bytecode_language()
prefix_filtert get_context(const optionst &options)
#define HELP_JAVA_METHOD_NAME
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_JAVA_GOTO_BINARY
#define HELP_JAVA_CLASSPATH
#define HELP_JAVA_CLASS_NAME
Goto Checker using Bounded Model Checking for Java.
Goto Checker using Bounded Model Checking for Java.
void parse_java_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the java object factory parameters from a given command line.
Goto Checker using Single Path Symbolic Execution for Java.
Goto Checker using Single Path Symbolic Execution for Java.
#define HELP_JAVA_TRACE_VALIDATION
JBMC Command Line Option Processing.
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
#define HELP_JSON_INTERFACE
Abstract interface to support a programming language.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
std::unique_ptr< T > util_make_unique(Ts &&... ts)
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
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.
std::string show_path_strategies()
suitable for displaying as a front-end help message
Storage of symbolic execution paths to resume.
int result_to_exit_code(resultt result)
resultt
The result of goto verifying.
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.
#define HELP_REACHABILITY_SLICER
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
Remove function exceptional returns.
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...
Remove Instance-of Operators.
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.
Remove Java New Operators.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
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...
Functions for replacing virtual function call with a static function calls in functions,...
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.
Replace Java Nondet expressions.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
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)
Java simple opaque stub generation.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define INITIALIZE_FUNCTION
Goto Verifier for stopping at the first failing property.
Goto Verifier for stopping at the first failing property and localizing the fault.
#define HELP_STRING_REFINEMENT
void set(const optionst &)
Assigns the parameters from given options.
const char * CBMC_VERSION
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE