97 options.
set_option(
"built-in-assertions",
true);
101 options.
set_option(
"show-goto-symex-steps",
false);
102 options.
set_option(
"show-points-to-sets",
false);
103 options.
set_option(
"show-array-constraints",
false);
127 <<
"--cover and --unwinding-assertions must not be given together"
135 "max-field-sensitivity-array-size",
144 <<
"--no-array-field-sensitivity and --max-field-sensitivity-array-size"
148 options.
set_option(
"no-array-field-sensitivity",
true);
155 <<
"--reachability-slice and --reachability-slice-fb must not be "
190 log.
warning() <<
"**** WARNING: Complexity-limited analysis may yield "
191 "unsound verification results"
195 if(
cmdline.
isset(
"symex-complexity-failed-child-loops-limit"))
198 "symex-complexity-failed-child-loops-limit",
202 log.
warning() <<
"**** WARNING: Complexity-limited analysis may yield "
203 "unsound verification results"
212 options.
set_option(
"drop-unused-functions",
true);
215 options.
set_option(
"havoc-undefined-functions",
true);
218 options.
set_option(
"string-abstraction",
true);
221 options.
set_option(
"reachability-slice-fb",
true);
224 options.
set_option(
"reachability-slice",
true);
250 if(options.
get_option(
"export-symex-ready-goto").empty())
253 <<
"ERROR: Please provide a filename to write the goto-binary to."
267 log.
warning() <<
"**** WARNING: Use --unwinding-assertions to obtain "
268 "sound verification results"
277 <<
"**** WARNING: Depth-bounded analysis may yield unsound verification "
294 log.
warning() <<
"**** WARNING: Use --unwinding-assertions to obtain "
295 "sound verification results"
306 "self-loops-to-assumptions",
315 options.
set_option(
"unwinding-assertions",
true);
316 options.
set_option(
"paths-symex-explore-all",
true);
323 <<
"**** WARNING: --partial-loops may yield unsound verification results"
337 options.
set_option(
"show-array-constraints",
true);
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"
382 "symex-coverage-report",
384 options.
set_option(
"paths-symex-explore-all",
true);
389 options.
set_option(
"validate-ssa-equation",
true);
394 options.
set_option(
"validate-goto-model",
true);
398 options.
set_option(
"show-goto-symex-steps",
true);
401 options.
set_option(
"show-points-to-sets",
true);
446 log.
error() <<
"This version of CBMC has no support for "
447 " hardware modules. Please use hw-cbmc."
456 log.
error() <<
"--show-points-to-sets supports only"
457 " json output. Use --json-ui."
467 log.
error() <<
"--show-array-constraints supports only"
468 " json output. Use --json-ui."
480 gcc_version.
get(
"gcc");
511 log.
error() <<
"failed to open input file '" << filename <<
"'"
516 std::unique_ptr<languaget> language=
519 if(language==
nullptr)
521 log.
error() <<
"failed to figure out type of file '" << filename <<
"'"
526 language->set_language_options(options);
531 if(language->parse(
infile, filename))
537 language->show_parse(std::cout);
560 if(options.
is_set(
"export-symex-ready-goto"))
563 options.
get_option(
"export-symex-ready-goto");
570 log.
error() <<
"ERROR: Unable to export goto-program in file "
576 log.
status() <<
"Exported goto-program in symex-ready-goto form at "
622 if(options.
is_set(
"cover"))
638 std::unique_ptr<goto_verifiert>
verifier =
nullptr;
640 if(options.
is_set(
"incremental-loop"))
709 const resultt result = (*verifier)();
787 std::ifstream
infile(filename);
796 language->set_language_options(options);
798 if(language ==
nullptr)
806 if(language->preprocess(
infile, filename, std::cout))
835 log.
status() <<
"Adding nondeterministic initialization "
836 "of static/global variables"
857 if(options.
is_set(
"cover"))
876 log.
status() <<
"Performing a forwards-backwards reachability slice"
878 if(options.
is_set(
"property"))
893 if(options.
is_set(
"property"))
907 log.
warning() <<
"**** WARNING: Experimental option --full-slice, "
908 <<
"analysis results may be unsound. See "
909 <<
"https://github.com/diffblue/cbmc/issues/260"
912 if(options.
is_set(
"property"))
937 "Usage: \tPurpose:\n"
939 " {bcbmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
940 " {bcbmc} {y--version} \t show version and exit\n"
941 " {bcbmc} [options] {ufile.c} {u...} \t perform bounded model checking\n"
943 "Analysis options:\n"
945 " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage"
947 " {y--property} {uid} \t only check one specific property\n"
948 " {y--trace} \t give a counterexample trace for failed properties\n"
949 " {y--stop-on-fail} \t stop analysis once a failed property is detected"
950 " (implies {y--trace})\n"
951 " {y--localize-faults} \t localize faults (experimental)\n"
953 "C/C++ frontend options:\n"
954 " {y--preprocess} \t stop after preprocessing\n"
955 " {y--test-preprocessor} \t stop after preprocessing, discard output\n"
960 "Platform options:\n"
963 "Program representations:\n"
964 " {y--show-parse-tree} \t show parse tree\n"
965 " {y--show-symbol-table} \t show loaded symbol table\n"
968 " {y--export-symex-ready-goto} {uf} \t "
969 "serialise goto-program in symex-ready-goto form in {uf}\n"
971 "Program instrumentation options:\n"
974 " {y--mm} {uMM} \t memory consistency model for concurrent programs"
975 " (default: {ysc})\n"
978 " {y--full-slice} \t run full slicer (experimental)\n"
979 " {y--drop-unused-functions} \t drop functions trivially unreachable from"
981 " {y--havoc-undefined-functions} \t for any function that has no body,"
982 " assign non-deterministic values to any parameters passed as non-const"
983 " pointers and the return value\n"
985 "Semantic transformations:\n"
986 " {y--nondet-static} \t add nondeterministic initialization of variables"
987 " with static lifetime\n"
996 " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
997 " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
999 " {y--show-array-constraints} \t show array theory constraints added"
1000 " during post processing. Requires {y--json-ui}.\n"
1002 "User-interface options:\n"
1007 " {y--verbosity} {u#} \t verbosity level\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, const symbol_table_baset &symbol_table, symbol_table_baset &dest_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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
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
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.
message_handlert & get_message_handler()
mstreamt & warning() const
mstreamt & status() const
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...
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, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
static void show_goto_functions(const goto_modelt &goto_model)
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 > &, const symbol_tablet &, 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, message_handlert &message_handler)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
#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.
#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_table_baset &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.
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
#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
#define widen_if_needed(s)
const char * CBMC_VERSION
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE