69 path_strategy_chooser()
76 const std::string &extra_options)
80 path_strategy_chooser()
89 options.
set_option(
"built-in-assertions",
true);
153 "localize-faults-method",
178 "self-loops-to-assumptions",
186 options.
set_option(
"java-unwind-enum-static",
true);
198 options.
set_option(
"unwinding-assertions",
true);
208 error() <<
"--partial-loops and --unwinding-assertions " 209 <<
"must not be given together" <<
eom;
239 options.
set_option(
"refine-arithmetic",
true);
246 options.
set_option(
"refine-arithmetic",
true);
256 warning() <<
"--string-printable ignored due to --no-refine-strings" 266 warning() <<
"--string-input-value ignored due to --no-refine-strings" 270 "string-input-value",
278 warning() <<
"--max-nondet-string-length ignored due to " 279 <<
"--no-refine-strings" <<
eom;
284 "max-node-refinement",
291 error() <<
"--smt1 is no longer supported" <<
eom;
301 bool solver_set=
false;
305 options.
set_option(
"boolector",
true), solver_set=
true;
311 options.
set_option(
"mathsat",
true), solver_set=
true;
317 options.
set_option(
"cvc4",
true), solver_set=
true;
323 options.
set_option(
"yices",
true), solver_set=
true;
329 options.
set_option(
"z3",
true), solver_set=
true;
351 options.
set_option(
"sat-preprocessor",
false);
369 "symex-coverage-report",
379 options.
set_option(
"symex-driven-lazy-loading",
true);
380 for(
const char *opt :
383 "reachability-slice",
384 "reachability-slice-fb" })
388 throw std::string(
"Option ") + opt +
389 " can't be used with --symex-driven-lazy-loading";
400 options.
set_option(
"allow-pointer-unsoundness",
true);
425 catch(
const char *error_msg)
431 catch(
const std::string &error_msg)
457 json_options[
"options"] = options.to_json();
458 debug() << json_options;
462 debug() << options.to_xml();
473 error() <<
"Please give exactly one source file" <<
eom;
480 std::ifstream infile(
widen(filename));
482 std::ifstream infile(filename);
487 error() <<
"failed to open input file `" 488 << filename <<
"'" <<
eom;
492 std::unique_ptr<languaget> language=
495 if(language==
nullptr)
497 error() <<
"failed to figure out type of file `" 498 << filename <<
"'" <<
eom;
505 status() <<
"Parsing " << filename <<
eom;
507 if(language->
parse(infile, filename))
517 std::function<void(bmct &, const symbol_tablet &)> configure_bmc =
nullptr;
518 if(options.get_bool_option(
"java-unwind-enum-static"))
524 unsigned loop_number,
526 unsigned &max_unwind) {
528 context, loop_number, unwind, max_unwind, symbol_table);
536 options.get_bool_option(
"java-assume-inputs-non-null");
540 std::unique_ptr<goto_modelt> goto_model_ptr;
542 if(get_goto_program_ret!=-1)
543 return get_goto_program_ret;
574 util_make_unique<class_hierarchyt>(lazy_goto_model.
symbol_table);
581 error() <<
"the program has no entry point";
593 auto callback_after_symex = [
this, &lazy_goto_model]() {
605 callback_after_symex);
623 catch(
const std::string &e)
638 std::unique_ptr<goto_modelt> &goto_model,
643 error() <<
"Please provide a program to verify" <<
eom;
654 util_make_unique<class_hierarchyt>(lazy_goto_model.
symbol_table);
686 std::move(lazy_goto_model));
687 if(goto_model ==
nullptr)
719 catch(
const std::string &e)
730 catch(
const std::bad_alloc &)
748 bool using_symex_driven_loading =
759 auto function_is_stub = [&symbol_table, &model](
const irep_idt &id) {
775 if(using_symex_driven_loading)
790 goto_check(ns, options, ID_java,
function.get_goto_function());
802 for(
const irep_idt &new_symbol_name : new_symbols)
813 if(using_symex_driven_loading)
818 goto_function.body.update();
819 function.compute_location_numbers();
820 goto_function.body.compute_loop_numbers();
824 function.update_instructions_function();
833 catch(
const std::string &e)
839 catch(
const std::bad_alloc &)
900 status() <<
"Running GOTO functions transformation passes" <<
eom;
902 bool using_symex_driven_loading =
907 if(using_symex_driven_loading)
921 status() <<
"Adding nondeterministic initialization " 922 "of static/global variables" <<
eom;
932 status() <<
"Removing unused functions" <<
eom;
951 error() <<
"--reachability-slice and --reachability-slice-fb " 952 <<
"must not be given together" <<
eom;
956 status() <<
"Performing a forwards-backwards reachability slice" <<
eom;
965 status() <<
"Performing a reachability slice" <<
eom;
975 status() <<
"Performing a full slice" <<
eom;
992 catch(
const std::string &e)
1003 catch(
const std::bad_alloc &)
1023 bool body_available)
1060 "* * Copyright (C) 2001-2018 * *\n" 1061 "* * Daniel Kroening, Edmund Clarke * *\n" 1062 "* * Carnegie Mellon University, Computer Science Department * *\n" 1063 "* * kroening@kroening.com * *\n" 1067 " jbmc [-?] [-h] [--help] show help\n" 1068 " jbmc class name of class or JAR file to be checked\n" 1069 " In the case of a JAR file, if a main class can be\n" 1070 " inferred from --main-class, --function, or the JAR\n" 1071 " manifest (checked in this order), the behavior is\n" 1072 " the same as running jbmc on the corresponding\n" 1075 "Analysis options:\n" 1077 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" 1078 " --property id only check one specific property\n" 1079 " --stop-on-fail stop analysis once a failed property is detected\n" 1080 " --trace give a counterexample trace for failed properties\n" 1084 "Program representations:\n" 1085 " --show-parse-tree show parse tree\n" 1086 " --show-symbol-table show loaded symbol table\n" 1087 " --list-symbols list symbols with type information\n" 1089 " --drop-unused-functions drop functions trivially unreachable\n" 1090 " from main function\n" 1093 "Program instrumentation options:\n" 1094 " --no-assertions ignore user assertions\n" 1095 " --no-assumptions ignore user assumptions\n" 1096 " --error-label label check that label is unreachable\n" 1097 " --mm MM memory consistency model for concurrent programs\n" 1099 " --full-slice run full slicer (experimental)\n" 1101 "Java Bytecode frontend options:\n" 1102 " --classpath dir/jar set the classpath\n" 1103 " --main-class class-name set the name of the main class\n" 1107 " --java-threading enable java multi-threading support (experimental)\n" 1108 " --java-unwind-enum-static unwind loops in static initialization of enums\n" 1110 " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" 1111 " execution. Note that --show-symbol-table,\n" 1112 " --show-goto-functions/properties output\n" 1113 " will be restricted to loaded methods in this case,\n" 1114 " and only output after the symex phase.\n" 1116 "Semantic transformations:\n" 1118 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 1123 "Backend options:\n" 1124 " --object-bits n number of bits used for object addresses\n" 1125 " --dimacs generate CNF in DIMACS format\n" 1126 " --beautify beautify the counterexample (greedy heuristic)\n" 1127 " --localize-faults localize faults (experimental)\n" 1128 " --smt1 use default SMT1 solver (obsolete)\n" 1129 " --smt2 use default SMT2 solver (Z3)\n" 1130 " --boolector use Boolector\n" 1131 " --mathsat use MathSAT\n" 1132 " --cvc4 use CVC4\n" 1133 " --yices use Yices\n" 1135 " --refine use refinement procedure (experimental)\n" 1137 " --outfile filename output formula to given file\n" 1138 " --arrays-uf-never never turn arrays into uninterpreted functions\n" 1139 " --arrays-uf-always always turn arrays into uninterpreted functions\n" 1142 " --version show version and exit\n" 1143 " --xml-ui use XML-formatted output\n" 1144 " --json-ui use JSON-formatted output\n" 1147 " --verbosity # verbosity level\n" Remove Java New Operators.
const std::list< std::string > & get_values(const std::string &option) const
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
jbmc_parse_optionst(int argc, const char **argv)
void convert_nondet(goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &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 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...
std::unique_ptr< class_hierarchyt > class_hierarchy
#define HELP_REACHABILITY_SLICER
Abstract interface to eager or lazy GOTO models.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Remove function exceptional returns.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Remove Instance-of Operators.
std::wstring widen(const char *s)
Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs.
irep_idt mode
Language mode.
std::string object_bits_info()
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...
static void set_default_options(optionst &)
Set the options that have default values.
#define HELP_SHOW_CLASS_HIERARCHY
Java simple opaque stub generation.
exprt value
Initial value of symbol.
std::string get_value(char option) const
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
JBMC Command Line Option Processing.
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
java_object_factory_parameterst object_factory_params
A GOTO model that produces function bodies on demand.
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
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 show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
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...
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, an lvalue, and doesn't already have one.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
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...
path_strategy_choosert path_strategy_chooser
Set the properties to check.
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
mstreamt & warning() const
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
bool set(const cmdlinet &cmdline)
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
virtual const symbol_tablet & get_symbol_table() const override
std::string show_strategies() const
suitable for displaying as a front-end help message
virtual bool isset(char option) const
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
void parse_java_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the java object factory parameters from a given command line.
bool can_generate_function_body(const irep_idt &name)
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
const changesett & get_inserted() const
#define INITIALIZE_FUNCTION
Nondeterministically initializes global scope variables, except for constants (such as string literal...
bool get_bool_option(const std::string &option) const
#define HELP_STRING_REFINEMENT
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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...
::goto_functiont goto_functiont
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
Abstract interface to support a programming language.
Convert side_effect_expr_nondett expressions using java_object_factory.
std::unique_ptr< languaget > new_java_bytecode_language()
virtual void set_message_handler(message_handlert &_message_handler)
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
virtual int doit() override
invoke main modules
Replace Java Nondet expressions.
std::string banner_string(const std::string &front_end, const std::string &version)
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
virtual void help() override
display command line help
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
void load_all_functions() const
Eagerly loads all functions from the symbol table.
int get_goto_program(std::unique_ptr< goto_modelt > &goto_model, const optionst &)
virtual void show_parse(std::ostream &out)=0
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
std::vector< framet > call_stackt
static irep_idt this_operating_system()
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand)...
message_handlert & get_message_handler()
bool stub_objects_are_not_null
Goto Programs with Functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
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 full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
bool set_properties(goto_modelt &goto_model)
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
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...
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
std::unordered_set< irep_idt > changesett
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...
void remove_java_new(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.
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
std::unique_ptr< languaget > new_ansi_c_language()
void set(const optionst &)
Assigns the parameters from given options.
Bounded model checking or path exploration for goto-programs.
Unwind loops in static initializers.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
virtual void set_language_options(const optionst &)
Set language-specific options.
ui_message_handlert ui_message_handler
void get_command_line_options(optionst &)
virtual void usage_error()
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
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 set_option(const std::string &option, const bool value)
virtual bool parse(std::istream &instream, const std::string &path)=0
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
void label_properties(goto_modelt &goto_model)
tvt java_enum_static_init_unwind_handler(const goto_symex_statet::call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table)
Unwind handler that special-cases the clinit (static initializer) functions of enumeration classes...
goto_functionst goto_functions
GOTO functions.
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)
static irep_idt this_architecture()
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 initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)