82 const std::string &extra_options)
96 options.
set_option(
"built-in-assertions",
true);
100 options.
set_option(
"show-goto-symex-steps",
false);
101 options.
set_option(
"show-points-to-sets",
false);
102 options.
set_option(
"show-array-constraints",
false);
116 options.
set_option(
"pointer-primitive-check", enabled);
117 options.
set_option(
"div-by-zero-check", enabled);
118 options.
set_option(
"signed-overflow-check", enabled);
119 options.
set_option(
"undefined-shift-check", enabled);
125 if(!options.
is_set(
"unwinding-assertions"))
127 options.
set_option(
"unwinding-assertions", enabled);
132 config.ansi_c.malloc_may_fail =
true;
133 config.ansi_c.malloc_failure_mode =
138 config.ansi_c.malloc_may_fail =
false;
139 config.ansi_c.malloc_failure_mode =
149 options, !
cmdline.isset(
"no-standard-checks"));
163 if(
cmdline.isset(
"cover") &&
cmdline.isset(
"unwinding-assertions"))
166 <<
"--cover and --unwinding-assertions must not be given together"
175 !
cmdline.isset(
"no-unwinding-assertions"))
177 log.warning() <<
"--cover is incompatible with --unwinding-assertions, so "
178 "unwinding-assertions will be defaulted to false"
189 if(
cmdline.isset(
"unwinding-assertions"))
191 options.
set_option(
"unwinding-assertions",
true);
192 options.
set_option(
"paths-symex-explore-all",
true);
194 else if(
cmdline.isset(
"no-unwinding-assertions"))
196 options.
set_option(
"unwinding-assertions",
false);
197 options.
set_option(
"paths-symex-explore-all",
false);
200 if(
cmdline.isset(
"max-field-sensitivity-array-size"))
203 "max-field-sensitivity-array-size",
204 cmdline.get_value(
"max-field-sensitivity-array-size"));
207 if(
cmdline.isset(
"no-array-field-sensitivity"))
209 if(
cmdline.isset(
"max-field-sensitivity-array-size"))
212 <<
"--no-array-field-sensitivity and --max-field-sensitivity-array-size"
216 options.
set_option(
"no-array-field-sensitivity",
true);
219 if(
cmdline.isset(
"reachability-slice") &&
220 cmdline.isset(
"reachability-slice-fb"))
223 <<
"--reachability-slice and --reachability-slice-fb must not be "
228 if(
cmdline.isset(
"full-slice"))
231 if(
cmdline.isset(
"show-symex-strategies"))
239 if(
cmdline.isset(
"program-only"))
242 if(
cmdline.isset(
"show-byte-ops"))
254 options.
set_option(
"unwinding-assertions",
false);
260 if(
cmdline.isset(
"symex-complexity-limit"))
263 "symex-complexity-limit",
cmdline.get_value(
"symex-complexity-limit"));
264 log.warning() <<
"**** WARNING: Complexity-limited analysis may yield "
265 "unsound verification results"
269 if(
cmdline.isset(
"symex-complexity-failed-child-loops-limit"))
272 "symex-complexity-failed-child-loops-limit",
273 cmdline.get_value(
"symex-complexity-failed-child-loops-limit"));
274 if(!
cmdline.isset(
"symex-complexity-limit"))
276 log.warning() <<
"**** WARNING: Complexity-limited analysis may yield "
277 "unsound verification results"
285 if(
cmdline.isset(
"drop-unused-functions"))
286 options.
set_option(
"drop-unused-functions",
true);
288 if(
cmdline.isset(
"string-abstraction"))
289 options.
set_option(
"string-abstraction",
true);
291 if(
cmdline.isset(
"reachability-slice-fb"))
292 options.
set_option(
"reachability-slice-fb",
true);
294 if(
cmdline.isset(
"reachability-slice"))
295 options.
set_option(
"reachability-slice",
true);
297 if(
cmdline.isset(
"nondet-static"))
300 if(
cmdline.isset(
"no-simplify"))
303 if(
cmdline.isset(
"stop-on-fail") ||
317 if(
cmdline.isset(
"export-symex-ready-goto"))
320 "export-symex-ready-goto",
cmdline.get_value(
"export-symex-ready-goto"));
321 if(options.
get_option(
"export-symex-ready-goto").empty())
324 <<
"ERROR: Please provide a filename to write the goto-binary to."
330 if(
cmdline.isset(
"localize-faults"))
338 !
cmdline.isset(
"unwinding-assertions"))
340 log.warning() <<
"**** WARNING: Use --unwinding-assertions to obtain "
341 "sound verification results"
350 <<
"**** WARNING: Depth-bounded analysis may yield unsound verification "
355 if(
cmdline.isset(
"slice-by-trace"))
364 "unwindset",
cmdline.get_comma_separated_values(
"unwindset"));
367 !
cmdline.isset(
"unwinding-assertions"))
369 log.warning() <<
"**** WARNING: Use --unwinding-assertions to obtain "
370 "sound verification results"
376 if(
cmdline.isset(
"no-propagation"))
381 "self-loops-to-assumptions",
382 !
cmdline.isset(
"no-self-loops-to-assumptions"));
387 if(
cmdline.isset(
"partial-loops"))
391 <<
"**** WARNING: --partial-loops may yield unsound verification results"
396 if(
cmdline.isset(
"slice-formula"))
399 if(
cmdline.isset(
"arrays-uf-always"))
401 else if(
cmdline.isset(
"arrays-uf-never"))
404 if(
cmdline.isset(
"show-array-constraints"))
405 options.
set_option(
"show-array-constraints",
true);
407 if(
cmdline.isset(
"refine-strings"))
414 "symex-cache-dereferences",
cmdline.isset(
"symex-cache-dereferences"));
416 if(
cmdline.isset(
"incremental-loop"))
419 "incremental-loop",
cmdline.get_value(
"incremental-loop"));
423 if(
cmdline.isset(
"unwind-min"))
426 if(
cmdline.isset(
"unwind-max"))
429 if(
cmdline.isset(
"ignore-properties-before-unwind-min"))
430 options.
set_option(
"ignore-properties-before-unwind-min",
true);
434 log.error() <<
"--paths not supported with --incremental-loop"
440 if(
cmdline.isset(
"graphml-witness"))
447 if(
cmdline.isset(
"symex-coverage-report"))
450 "symex-coverage-report",
451 cmdline.get_value(
"symex-coverage-report"));
452 options.
set_option(
"paths-symex-explore-all",
true);
455 if(
cmdline.isset(
"validate-ssa-equation"))
457 options.
set_option(
"validate-ssa-equation",
true);
460 if(
cmdline.isset(
"validate-goto-model"))
462 options.
set_option(
"validate-goto-model",
true);
465 if(
cmdline.isset(
"show-goto-symex-steps"))
466 options.
set_option(
"show-goto-symex-steps",
true);
468 if(
cmdline.isset(
"show-points-to-sets"))
469 options.
set_option(
"show-points-to-sets",
true);
512 cmdline.isset(
"gen-interface"))
514 log.error() <<
"This version of CBMC has no support for "
515 " hardware modules. Please use hw-cbmc."
520 if(
cmdline.isset(
"show-points-to-sets"))
524 log.error() <<
"--show-points-to-sets supports only"
525 " json output. Use --json-ui."
531 if(
cmdline.isset(
"show-array-constraints"))
535 log.error() <<
"--show-array-constraints supports only"
536 " json output. Use --json-ui."
548 gcc_version.
get(
"gcc");
552 if(
cmdline.isset(
"test-preprocessor"))
557 if(
cmdline.isset(
"preprocess"))
563 if(
cmdline.isset(
"show-parse-tree"))
573 std::string filename=
cmdline.args[0];
579 log.error() <<
"failed to open input file '" << filename <<
"'"
584 std::unique_ptr<languaget> language=
587 if(language==
nullptr)
589 log.error() <<
"failed to figure out type of file '" << filename <<
"'"
608 int get_goto_program_ret =
611 if(get_goto_program_ret!=-1)
612 return get_goto_program_ret;
614 if(
cmdline.isset(
"show-claims") ||
615 cmdline.isset(
"show-properties"))
627 if(options.
is_set(
"export-symex-ready-goto"))
629 auto symex_ready_goto_filename =
630 options.
get_option(
"export-symex-ready-goto");
637 log.error() <<
"ERROR: Unable to export goto-program in file "
643 log.status() <<
"Exported goto-program in symex-ready-goto form at "
689 if(options.
is_set(
"cover"))
705 std::unique_ptr<goto_verifiert> verifier =
nullptr;
707 if(options.
is_set(
"incremental-loop"))
711 verifier = std::make_unique<
726 std::make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
742 std::make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
750 verifier = std::make_unique<
766 verifier = std::make_unique<
776 const resultt result = (*verifier)();
810 if(
cmdline.isset(
"show-symbol-table"))
819 if(
cmdline.isset(
"validate-goto-model"))
825 if(
cmdline.isset(
"show-loops"))
833 cmdline.isset(
"show-goto-functions") ||
834 cmdline.isset(
"list-goto-functions"))
854 std::string filename =
cmdline.args[0];
856 std::ifstream infile(filename);
866 if(language ==
nullptr)
888 log.status() <<
"Adding CPROVER library (" <<
config.ansi_c.arch <<
")"
912 log.status() <<
"Adding nondeterministic initialization "
913 "of static/global variables"
934 if(options.
is_set(
"cover"))
937 options,
goto_model.symbol_table,
log.get_message_handler());
953 log.status() <<
"Performing a forwards-backwards reachability slice"
955 if(options.
is_set(
"property"))
961 log.get_message_handler());
970 if(options.
is_set(
"property"))
975 log.get_message_handler());
984 log.warning() <<
"**** WARNING: Experimental option --full-slice, "
985 <<
"analysis results may be unsound. See "
986 <<
"https://github.com/diffblue/cbmc/issues/260"
989 if(options.
is_set(
"property"))
993 log.get_message_handler());
1017 "Usage: \tPurpose:\n"
1019 " {bcbmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
1020 " {bcbmc} {y--version} \t show version and exit\n"
1021 " {bcbmc} [options] {ufile.c} {u...} \t perform bounded model checking\n"
1023 "Analysis options:\n"
1025 " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage"
1027 " {y--property} {uid} \t only check one specific property\n"
1028 " {y--trace} \t give a counterexample trace for failed properties\n"
1029 " {y--stop-on-fail} \t stop analysis once a failed property is detected"
1030 " (implies {y--trace})\n"
1031 " {y--localize-faults} \t localize faults (experimental)\n"
1033 "C/C++ frontend options:\n"
1034 " {y--preprocess} \t stop after preprocessing\n"
1035 " {y--test-preprocessor} \t stop after preprocessing, discard output\n"
1040 "Platform options:\n"
1043 "Program representations:\n"
1044 " {y--show-parse-tree} \t show parse tree\n"
1045 " {y--show-symbol-table} \t show loaded symbol table\n"
1048 " {y--export-symex-ready-goto} {uf} \t "
1049 "serialise goto-program in symex-ready-goto form in {uf}\n"
1051 "Program instrumentation options:\n"
1054 " {y--mm} {uMM} \t memory consistency model for concurrent programs"
1055 " (default: {ysc})\n"
1058 " {y--full-slice} \t run full slicer (experimental)\n"
1059 " {y--drop-unused-functions} \t drop functions trivially unreachable from"
1062 "Semantic transformations:\n"
1063 " {y--nondet-static} \t add nondeterministic initialization of variables"
1064 " with static lifetime\n"
1069 "Backend options:\n"
1073 " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
1074 " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
1076 " {y--show-array-constraints} \t show array theory constraints added"
1077 " during post processing. Requires {y--json-ui}.\n"
1079 "User-interface options:\n"
1084 " {y--verbosity} {u#} \t verbosity level (default 6)\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.
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 &)
static void set_default_analysis_flags(optionst &, const bool enabled)
Setup default analysis flags.
virtual void help() override
display command line help
cbmc_parse_optionst(int argc, const char **argv)
void report() override
Report results.
const goto_trace_storaget & get_traces() const
void get(const std::string &executable)
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.
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()
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
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.
#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 property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties, message_handlert &message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
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)
void update_max_malloc_size(goto_modelt &goto_model, message_handlert &message_handler)
Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed.
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< 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_modelt &goto_model, 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, message_handlert &message_handler)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
bool has_asm(const goto_functionst &goto_functions)
returns true iff the given goto functions use asm instructions
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
@ malloc_failure_mode_return_null
@ malloc_failure_mode_none
#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