Go to the documentation of this file.
101 const std::string &extra_options)
117 options.
set_option(
"built-in-assertions",
true);
124 options.
set_option(
"show-goto-symex-steps",
false);
147 <<
"--cover and --unwinding-assertions must not be given together"
155 "max-field-sensitivity-array-size",
164 <<
"--no-array-field-sensitivity and --max-field-sensitivity-array-size"
168 options.
set_option(
"no-array-field-sensitivity",
true);
174 <<
"--partial-loops and --unwinding-assertions must not be given "
183 <<
"--reachability-slice and --reachability-slice-fb must not be "
221 if(
cmdline.
isset(
"symex-complexity-failed-child-loops-limit"))
223 "symex-complexity-failed-child-loops-limit",
245 options.
set_option(
"drop-unused-functions",
true);
248 options.
set_option(
"havoc-undefined-functions",
true);
251 options.
set_option(
"string-abstraction",
true);
254 options.
set_option(
"reachability-slice-fb",
true);
257 options.
set_option(
"reachability-slice",
true);
306 "self-loops-to-assumptions",
327 options.
set_option(
"unwinding-assertions",
true);
328 options.
set_option(
"paths-symex-explore-all",
true);
359 options.
set_option(
"refine-arithmetic",
true);
366 options.
set_option(
"refine-arithmetic",
true);
377 "max-node-refinement",
393 if(
cmdline.
isset(
"ignore-properties-before-unwind-min"))
394 options.
set_option(
"ignore-properties-before-unwind-min",
true);
398 log.
error() <<
"--paths not supported with --incremental-loop"
418 bool solver_set=
false;
422 options.
set_option(
"boolector",
true), solver_set=
true;
428 options.
set_option(
"cprover-smt2",
true), solver_set =
true;
434 options.
set_option(
"mathsat",
true), solver_set=
true;
440 options.
set_option(
"cvc4",
true), solver_set=
true;
453 options.
set_option(
"yices",
true), solver_set=
true;
459 options.
set_option(
"z3",
true), solver_set=
true;
487 options.
set_option(
"sat-preprocessor",
false);
505 "symex-coverage-report",
507 options.
set_option(
"paths-symex-explore-all",
true);
512 options.
set_option(
"validate-ssa-equation",
true);
517 options.
set_option(
"validate-goto-model",
true);
521 options.
set_option(
"show-goto-symex-steps",
true);
559 log.
error() <<
"This version of CBMC has no support for "
560 " hardware modules. Please use hw-cbmc."
571 gcc_version.
get(
"gcc");
599 std::ifstream infile(
widen(filename));
601 std::ifstream infile(filename);
606 log.
error() <<
"failed to open input file '" << filename <<
"'"
611 std::unique_ptr<languaget> language=
614 if(language==
nullptr)
616 log.
error() <<
"failed to figure out type of file '" << filename <<
"'"
626 if(language->
parse(infile, filename))
636 int get_goto_program_ret =
639 if(get_goto_program_ret!=-1)
640 return get_goto_program_ret;
692 if(options.
is_set(
"cover"))
705 std::unique_ptr<goto_verifiert> verifier =
nullptr;
707 if(options.
is_set(
"incremental-loop"))
726 util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
742 util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
776 const resultt result = (*verifier)();
854 std::ifstream infile(filename);
865 if(language ==
nullptr)
873 if(language->
preprocess(infile, filename, std::cout))
900 log.
status() <<
"Removal of function pointers and virtual functions"
929 log.
status() <<
"Adding nondeterministic initialization "
930 "of static/global variables"
963 if(options.
is_set(
"cover"))
982 log.
status() <<
"Performing a forwards-backwards reachability slice"
984 if(options.
is_set(
"property"))
994 if(options.
is_set(
"property"))
1004 if(options.
is_set(
"property"))
1030 " cbmc [-?] [-h] [--help] show help\n"
1031 " cbmc file.c ... source file names\n"
1033 "Analysis options:\n"
1035 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n"
1036 " --property id only check one specific property\n"
1037 " --stop-on-fail stop analysis once a failed property is detected\n"
1038 " --trace give a counterexample trace for failed properties\n"
1040 "C/C++ frontend options:\n"
1041 " -I path set include path (C/C++)\n"
1042 " -D macro define preprocessor macro (C/C++)\n"
1043 " --preprocess stop after preprocessing\n"
1044 " --16, --32, --64 set width of int\n"
1045 " --LP64, --ILP64, --LLP64,\n"
1046 " --ILP32, --LP32 set width of int, long and pointers\n"
1047 " --little-endian allow little-endian word-byte conversions\n"
1048 " --big-endian allow big-endian word-byte conversions\n"
1049 " --unsigned-char make \"char\" unsigned by default\n"
1050 " --mm model set memory model (default: sc)\n"
1051 " --arch set architecture (default: "
1053 " --os set operating system (default: "
1055 " --c89/99/11 set C language standard (default: "
1062 " --cpp98/03/11 set C++ language standard (default: "
1070 " --gcc use GCC as preprocessor\n"
1072 " --no-arch don't set up an architecture\n"
1073 " --no-library disable built-in abstract C library\n"
1074 " --round-to-nearest rounding towards nearest even (default)\n"
1075 " --round-to-plus-inf rounding towards plus infinity\n"
1076 " --round-to-minus-inf rounding towards minus infinity\n"
1077 " --round-to-zero rounding towards zero\n"
1081 "Program representations:\n"
1082 " --show-parse-tree show parse tree\n"
1083 " --show-symbol-table show loaded symbol table\n"
1086 "Program instrumentation options:\n"
1088 " --no-assertions ignore user assertions\n"
1089 " --no-assumptions ignore user assumptions\n"
1090 " --error-label label check that label is unreachable\n"
1091 " --cover CC create test-suite with coverage criterion CC\n"
1092 " --mm MM memory consistency model for concurrent programs\n"
1094 " --malloc-fail-assert set malloc failure mode to assert-then-assume\n"
1095 " --malloc-fail-null set malloc failure mode to return null\n"
1097 " --malloc-may-fail allow malloc calls to return a null pointer\n"
1100 " --full-slice run full slicer (experimental)\n"
1101 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1102 " --havoc-undefined-functions\n"
1103 " for any function that has no body, assign non-deterministic values to\n"
1104 " any parameters passed as non-const pointers and the return value\n"
1106 "Semantic transformations:\n"
1108 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1113 "Backend options:\n"
1114 " --object-bits n number of bits used for object addresses\n"
1115 " --dimacs generate CNF in DIMACS format\n"
1116 " --beautify beautify the counterexample (greedy heuristic)\n"
1117 " --localize-faults localize faults (experimental)\n"
1118 " --smt2 use default SMT2 solver (Z3)\n"
1119 " --boolector use Boolector\n"
1120 " --cprover-smt2 use CPROVER SMT2 solver\n"
1121 " --cvc4 use CVC4\n"
1122 " --mathsat use MathSAT\n"
1123 " --yices use Yices\n"
1125 " --refine use refinement procedure (experimental)\n"
1126 " --external-sat-solver cmd command to invoke SAT solver process\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"
1141 " --write-solver-stats-to json-file\n"
1142 " collect the solver query complexity\n"
Class that provides messages with a built-in verbosity 'level'.
virtual int doit() override
invoke main modules
#define UNREACHABLE
This should be used to mark dead code.
Coverage Instrumentation.
#define HELP_REACHABILITY_SLICER
#define HELP_SHOW_GOTO_FUNCTIONS
virtual void show_parse(std::ostream &out)=0
std::string object_bits_info()
void get(const std::string &executable)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
ui_message_handlert ui_message_handler
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and...
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
resultt
The result of goto verifying.
virtual bool isset(char option) const
Stops when the first failing property is found.
const std::string get_option(const std::string &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
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
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 remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
const goto_trace_storaget & get_traces() const
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
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 configure_gcc(const gcc_versiont &gcc_version)
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)
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
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 show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
struct configt::ansi_ct ansi_c
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
cbmc_parse_optionst(int argc, const char **argv)
Nondeterministically initializes global scope variables, except for constants (such as string literal...
#define HELP_REACHABILITY_SLICER_FB
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.
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 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.
void register_languages()
#define HELP_JSON_INTERFACE
virtual uit get_ui() const
virtual void usage_error()
static void remove_vector(typet &)
removes vector data type
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Bounded Model Checking Utilities.
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.
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
const char * CBMC_VERSION
Goto verifier for covering goals that stores traces.
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the sta...
Goto verifier for verifying all properties that stores traces.
Initialize a Goto Program.
std::string banner_string(const std::string &front_end, const std::string &version)
Perform Memory-mapped I/O instrumentation.
CBMC Command Line Option Processing.
void get_command_line_options(optionst &)
preprocessort preprocessor
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Goto Checker using Multi-Path Symbolic Execution.
std::string get_value(char option) const
virtual bool parse(std::istream &instream, const std::string &path)=0
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
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.
virtual void set_message_handler(message_handlert &_message_handler)
#define HELP_SHOW_PROPERTIES
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Goto Checker using Single Path Symbolic Execution.
static irep_idt this_operating_system()
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
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.
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
void compute_loop_numbers()
#define HELP_STRING_REFINEMENT_CBMC
std::wstring widen(const char *s)
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,...
static c_standardt default_c_standard()
#define HELP_ANSI_C_LANGUAGE
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
Remove the 'vector' data type by compilation into arrays.
static void remove_complex(typet &)
removes complex data type
virtual void report()=0
Report results.
Replace function returns by assignments to global variables.
static irep_idt this_architecture()
message_handlert & get_message_handler()
int result_to_exit_code(resultt result)
goto_functionst goto_functions
GOTO functions.
Goto Verifier for stopping at the first failing property.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
bool set(const cmdlinet &cmdline)
static cpp_standardt default_cpp_standard()
Document and give macros for the exit codes of CPROVER binaries.
bool get_bool_option(const std::string &option) const
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
virtual void help() override
display command line help
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
std::string show_path_strategies()
suitable for displaying as a front-end help message
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 bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
#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)
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.
static void set_default_options(optionst &)
Set the options that have default values.
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)
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
const std::list< std::string > & get_values(const std::string &option) const
Remove Indirect Function Calls.
void report() override
Report results.
symbol_tablet symbol_table
Symbol table.
Goto Checker using Single Path Symbolic Execution only.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
const value_listt & get_list_option(const std::string &option) const
#define HELP_XML_INTERFACE
void preprocessing(const optionst &)
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
bool test_c_preprocessor(message_handlert &message_handler)