92 const std::string &extra_options)
106 options.
set_option(
"built-in-assertions",
true);
113 options.
set_option(
"show-goto-symex-steps",
false);
114 options.
set_option(
"show-points-to-sets",
false);
115 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;
428 options.
set_option(
"yices",
true), solver_set=
true;
434 options.
set_option(
"z3",
true), solver_set=
true;
462 options.
set_option(
"sat-preprocessor",
false);
480 "symex-coverage-report",
482 options.
set_option(
"paths-symex-explore-all",
true);
487 options.
set_option(
"validate-ssa-equation",
true);
492 options.
set_option(
"validate-goto-model",
true);
496 options.
set_option(
"show-goto-symex-steps",
true);
499 options.
set_option(
"show-points-to-sets",
true);
535 log.
error() <<
"This version of CBMC has no support for "
536 " hardware modules. Please use hw-cbmc."
545 log.
error() <<
"--show-points-to-sets supports only"
546 " json output. Use --json-ui."
556 log.
error() <<
"--show-array-constraints supports only"
557 " json output. Use --json-ui."
569 gcc_version.
get(
"gcc");
597 std::ifstream infile(
widen(filename));
599 std::ifstream infile(filename);
604 log.
error() <<
"failed to open input file '" << filename <<
"'"
609 std::unique_ptr<languaget> language=
612 if(language==
nullptr)
614 log.
error() <<
"failed to figure out type of file '" << filename <<
"'"
619 language->set_language_options(options);
624 if(language->parse(infile, filename))
630 language->show_parse(std::cout);
634 int get_goto_program_ret =
637 if(get_goto_program_ret!=-1)
638 return get_goto_program_ret;
690 if(options.
is_set(
"cover"))
706 std::unique_ptr<goto_verifiert> verifier =
nullptr;
708 if(options.
is_set(
"incremental-loop"))
727 util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
743 util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
777 const resultt result = (*verifier)();
855 std::ifstream infile(filename);
864 language->set_language_options(options);
866 if(language ==
nullptr)
874 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 " --incremental-smt2-solver cmd\n"
1051 " command to invoke external SMT solver for\n"
1052 " incremental solving (experimental)\n"
1053 " --external-sat-solver cmd command to invoke SAT solver process\n"
1055 " --outfile filename output formula to given file\n"
1056 " --arrays-uf-never never turn arrays into uninterpreted functions\n"
1057 " --arrays-uf-always always turn arrays into uninterpreted functions\n"
1060 " --version show version and exit\n"
1066 " --verbosity # verbosity level\n"
1068 " --write-solver-stats-to json-file\n"
1069 " collect the solver query complexity\n"
1070 " --show-array-constraints show array theory constraints added\n"
1071 " during post processing.\n"
1072 " Requires --json-ui.\n"
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....
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.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
Bounded Model Checking Utilities.
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
bool test_c_preprocessor(message_handlert &message_handler)
CBMC Command Line Option Processing.
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
virtual int doit() override
invoke main modules
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
static void set_default_options(optionst &)
Set the options that have default values.
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
void get_command_line_options(optionst &)
void register_languages() override
void preprocessing(const optionst &)
virtual void help() override
display command line help
cbmc_parse_optionst(int argc, const char **argv)
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::ansi_ct ansi_c
const goto_trace_storaget & get_traces() const
void report() override
Report results.
void get(const std::string &executable)
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.
symbol_tablet symbol_table
Symbol table.
Class that provides messages with a built-in verbosity 'level'.
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.
mstreamt & status() const
message_handlert & get_message_handler()
Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the sta...
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
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
const value_listt & get_list_option(const std::string &option) const
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
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and...
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
Stops when the first failing property is found.
virtual uit get_ui() const
#define HELP_CONFIG_LIBRARY
#define HELP_CONFIG_PLATFORM
#define HELP_CONFIG_C_CPP
#define HELP_CONFIG_BACKEND
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.
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 parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Coverage Instrumentation.
Goto verifier for covering goals that stores traces.
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
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_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.
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
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 configure_gcc(const gcc_versiont &gcc_version)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
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 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.
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_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Goto Checker using Multi-Path Symbolic Execution.
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
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_FB
#define HELP_REACHABILITY_SLICER
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
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...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
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 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)
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
Goto Checker using Single Path Symbolic Execution.
Goto Checker using Single Path Symbolic Execution only.
#define UNREACHABLE
This should be used to mark dead code.
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_CBMC
preprocessort preprocessor
std::wstring widen(const char *s)
const char * CBMC_VERSION
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE