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",
358 if(
cmdline.
isset(
"ignore-properties-before-unwind-min"))
359 options.
set_option(
"ignore-properties-before-unwind-min",
true);
363 log.
error() <<
"--paths not supported with --incremental-loop"
383 bool solver_set=
false;
387 options.
set_option(
"boolector",
true), solver_set=
true;
393 options.
set_option(
"cprover-smt2",
true), solver_set =
true;
399 options.
set_option(
"mathsat",
true), solver_set=
true;
405 options.
set_option(
"cvc4",
true), solver_set=
true;
418 options.
set_option(
"yices",
true), solver_set=
true;
424 options.
set_option(
"z3",
true), solver_set=
true;
452 options.
set_option(
"sat-preprocessor",
false);
470 "symex-coverage-report",
472 options.
set_option(
"paths-symex-explore-all",
true);
477 options.
set_option(
"validate-ssa-equation",
true);
482 options.
set_option(
"validate-goto-model",
true);
486 options.
set_option(
"show-goto-symex-steps",
true);
489 options.
set_option(
"show-points-to-sets",
true);
530 log.
error() <<
"This version of CBMC has no support for "
531 " hardware modules. Please use hw-cbmc."
540 log.
error() <<
"--show-points-to-sets supports only"
541 " json output. Use --json-ui."
551 log.
error() <<
"--show-array-constraints supports only"
552 " json output. Use --json-ui."
564 gcc_version.
get(
"gcc");
592 std::ifstream infile(
widen(filename));
594 std::ifstream infile(filename);
599 log.
error() <<
"failed to open input file '" << filename <<
"'"
604 std::unique_ptr<languaget> language=
607 if(language==
nullptr)
609 log.
error() <<
"failed to figure out type of file '" << filename <<
"'"
614 language->set_language_options(options);
619 if(language->parse(infile, filename))
625 language->show_parse(std::cout);
629 int get_goto_program_ret =
632 if(get_goto_program_ret!=-1)
633 return get_goto_program_ret;
685 if(options.
is_set(
"cover"))
701 std::unique_ptr<goto_verifiert> verifier =
nullptr;
703 if(options.
is_set(
"incremental-loop"))
722 util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
738 util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
772 const resultt result = (*verifier)();
850 std::ifstream infile(filename);
859 language->set_language_options(options);
861 if(language ==
nullptr)
869 if(language->preprocess(infile, filename, std::cout))
900 log.
status() <<
"Adding nondeterministic initialization "
901 "of static/global variables"
922 if(options.
is_set(
"cover"))
941 log.
status() <<
"Performing a forwards-backwards reachability slice"
943 if(options.
is_set(
"property"))
953 if(options.
is_set(
"property"))
963 if(options.
is_set(
"property"))
989 " cbmc [-?] [-h] [--help] show help\n"
990 " cbmc file.c ... source file names\n"
992 "Analysis options:\n"
994 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n"
995 " --property id only check one specific property\n"
996 " --trace give a counterexample trace for failed properties\n"
997 " --stop-on-fail stop analysis once a failed property is detected\n"
998 " (implies --trace)\n"
1000 "C/C++ frontend options:\n"
1001 " --preprocess stop after preprocessing\n"
1006 "Platform options:\n"
1009 "Program representations:\n"
1010 " --show-parse-tree show parse tree\n"
1011 " --show-symbol-table show loaded symbol table\n"
1014 "Program instrumentation options:\n"
1017 " --mm MM memory consistency model for concurrent programs (default: sc)\n"
1021 " --full-slice run full slicer (experimental)\n"
1022 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1023 " --havoc-undefined-functions\n"
1024 " for any function that has no body, assign non-deterministic values to\n"
1025 " any parameters passed as non-const pointers and the return value\n"
1027 "Semantic transformations:\n"
1029 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1034 "Backend options:\n"
1036 " --dimacs generate CNF in DIMACS format\n"
1037 " --beautify beautify the counterexample (greedy heuristic)\n"
1038 " --localize-faults localize faults (experimental)\n"
1039 " --smt2 use default SMT2 solver (Z3)\n"
1040 " --boolector use Boolector\n"
1041 " --cprover-smt2 use CPROVER SMT2 solver\n"
1042 " --cvc4 use CVC4\n"
1043 " --mathsat use MathSAT\n"
1044 " --yices use Yices\n"
1046 " --refine use refinement procedure (experimental)\n"
1047 " --external-sat-solver cmd command to invoke SAT solver process\n"
1049 " --outfile filename output formula to given file\n"
1050 " --arrays-uf-never never turn arrays into uninterpreted functions\n"
1051 " --arrays-uf-always always turn arrays into uninterpreted functions\n"
1054 " --version show version and exit\n"
1060 " --verbosity # verbosity level\n"
1062 " --write-solver-stats-to json-file\n"
1063 " collect the solver query complexity\n"
1064 " --show-array-constraints show array theory constraints added\n"
1065 " during post processing.\n"
1066 " 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....
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 ...
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 preprocessing(const optionst &)
virtual void help() override
display command line help
void register_languages()
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()
static irep_idt this_architecture()
static irep_idt this_operating_system()
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()
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)
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