Go to the documentation of this file.
93 const std::string &extra_options)
107 options.
set_option(
"built-in-assertions",
true);
114 options.
set_option(
"show-goto-symex-steps",
false);
115 options.
set_option(
"show-points-to-sets",
false);
116 options.
set_option(
"show-array-constraints",
false);
139 <<
"--cover and --unwinding-assertions must not be given together"
147 "max-field-sensitivity-array-size",
156 <<
"--no-array-field-sensitivity and --max-field-sensitivity-array-size"
160 options.
set_option(
"no-array-field-sensitivity",
true);
166 <<
"--partial-loops and --unwinding-assertions must not be given "
175 <<
"--reachability-slice and --reachability-slice-fb must not be "
210 if(
cmdline.
isset(
"symex-complexity-failed-child-loops-limit"))
212 "symex-complexity-failed-child-loops-limit",
219 options.
set_option(
"drop-unused-functions",
true);
222 options.
set_option(
"havoc-undefined-functions",
true);
225 options.
set_option(
"string-abstraction",
true);
228 options.
set_option(
"reachability-slice-fb",
true);
231 options.
set_option(
"reachability-slice",
true);
280 "self-loops-to-assumptions",
289 options.
set_option(
"unwinding-assertions",
true);
290 options.
set_option(
"paths-symex-explore-all",
true);
313 options.
set_option(
"show-array-constraints",
true);
324 options.
set_option(
"refine-arithmetic",
true);
331 options.
set_option(
"refine-arithmetic",
true);
342 "max-node-refinement",
346 "symex-cache-dereferences",
cmdline.
isset(
"symex-cache-dereferences"));
361 if(
cmdline.
isset(
"ignore-properties-before-unwind-min"))
362 options.
set_option(
"ignore-properties-before-unwind-min",
true);
366 log.
error() <<
"--paths not supported with --incremental-loop"
386 bool solver_set=
false;
390 options.
set_option(
"boolector",
true), solver_set=
true;
396 options.
set_option(
"cprover-smt2",
true), solver_set =
true;
402 options.
set_option(
"mathsat",
true), solver_set=
true;
408 options.
set_option(
"cvc4",
true), solver_set=
true;
421 options.
set_option(
"yices",
true), solver_set=
true;
427 options.
set_option(
"z3",
true), solver_set=
true;
455 options.
set_option(
"sat-preprocessor",
false);
473 "symex-coverage-report",
475 options.
set_option(
"paths-symex-explore-all",
true);
480 options.
set_option(
"validate-ssa-equation",
true);
485 options.
set_option(
"validate-goto-model",
true);
489 options.
set_option(
"show-goto-symex-steps",
true);
492 options.
set_option(
"show-points-to-sets",
true);
533 log.
error() <<
"This version of CBMC has no support for "
534 " hardware modules. Please use hw-cbmc."
543 log.
error() <<
"--show-points-to-sets supports only"
544 " json output. Use --json-ui."
554 log.
error() <<
"--show-array-constraints supports only"
555 " json output. Use --json-ui."
567 gcc_version.
get(
"gcc");
595 std::ifstream infile(
widen(filename));
597 std::ifstream infile(filename);
602 log.
error() <<
"failed to open input file '" << filename <<
"'"
607 std::unique_ptr<languaget> language=
610 if(language==
nullptr)
612 log.
error() <<
"failed to figure out type of file '" << filename <<
"'"
622 if(language->
parse(infile, filename))
632 int get_goto_program_ret =
635 if(get_goto_program_ret!=-1)
636 return get_goto_program_ret;
688 if(options.
is_set(
"cover"))
704 std::unique_ptr<goto_verifiert> verifier =
nullptr;
706 if(options.
is_set(
"incremental-loop"))
725 util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
741 util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
775 const resultt result = (*verifier)();
853 std::ifstream infile(filename);
864 if(language ==
nullptr)
872 if(language->
preprocess(infile, filename, std::cout))
903 log.
status() <<
"Adding nondeterministic initialization "
904 "of static/global variables"
925 if(options.
is_set(
"cover"))
944 log.
status() <<
"Performing a forwards-backwards reachability slice"
946 if(options.
is_set(
"property"))
956 if(options.
is_set(
"property"))
966 if(options.
is_set(
"property"))
992 " cbmc [-?] [-h] [--help] show help\n"
993 " cbmc file.c ... source file names\n"
995 "Analysis options:\n"
997 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n"
998 " --property id only check one specific property\n"
999 " --trace give a counterexample trace for failed properties\n"
1000 " --stop-on-fail stop analysis once a failed property is detected\n"
1001 " (implies --trace)\n"
1003 "C/C++ frontend options:\n"
1004 " --preprocess stop after preprocessing\n"
1009 "Platform options:\n"
1012 "Program representations:\n"
1013 " --show-parse-tree show parse tree\n"
1014 " --show-symbol-table show loaded symbol table\n"
1017 "Program instrumentation options:\n"
1020 " --mm MM memory consistency model for concurrent programs (default: sc)\n"
1024 " --full-slice run full slicer (experimental)\n"
1025 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1026 " --havoc-undefined-functions\n"
1027 " for any function that has no body, assign non-deterministic values to\n"
1028 " any parameters passed as non-const pointers and the return value\n"
1030 "Semantic transformations:\n"
1032 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1037 "Backend options:\n"
1039 " --dimacs generate CNF in DIMACS format\n"
1040 " --beautify beautify the counterexample (greedy heuristic)\n"
1041 " --localize-faults localize faults (experimental)\n"
1042 " --smt2 use default SMT2 solver (Z3)\n"
1043 " --boolector use Boolector\n"
1044 " --cprover-smt2 use CPROVER SMT2 solver\n"
1045 " --cvc4 use CVC4\n"
1046 " --mathsat use MathSAT\n"
1047 " --yices use Yices\n"
1049 " --refine use refinement procedure (experimental)\n"
1050 " --external-sat-solver cmd command to invoke SAT solver process\n"
1052 " --outfile filename output formula to given file\n"
1053 " --arrays-uf-never never turn arrays into uninterpreted functions\n"
1054 " --arrays-uf-always always turn arrays into uninterpreted functions\n"
1057 " --version show version and exit\n"
1063 " --verbosity # verbosity level\n"
1065 " --write-solver-stats-to json-file\n"
1066 " collect the solver query complexity\n"
1067 " --show-array-constraints show array theory constraints added\n"
1068 " during post processing.\n"
1069 " Requires --json-ui.\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
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
#define HELP_CONFIG_PLATFORM
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 set_option(const std::string &option, const bool value)
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()
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Bounded Model Checking Utilities.
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.
#define HELP_CONFIG_C_CPP
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)
CBMC Command Line Option Processing.
void get_command_line_options(optionst &)
preprocessort preprocessor
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.
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)
#define HELP_CONFIG_LIBRARY
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.
#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,...
#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 ...
virtual void report()=0
Report results.
static irep_idt this_architecture()
message_handlert & get_message_handler()
int result_to_exit_code(resultt result)
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)
Document and give macros for the exit codes of CPROVER binaries.
bool get_bool_option(const std::string &option) const
#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)
#define HELP_CONFIG_BACKEND
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.
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
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)