Go to the documentation of this file.
100 const std::string &extra_options)
116 options.
set_option(
"built-in-assertions",
true);
123 options.
set_option(
"show-goto-symex-steps",
false);
146 <<
"--cover and --unwinding-assertions must not be given together"
154 "max-field-sensitivity-array-size",
163 <<
"--no-array-field-sensitivity and --max-field-sensitivity-array-size"
167 options.
set_option(
"no-array-field-sensitivity",
true);
173 <<
"--partial-loops and --unwinding-assertions must not be given "
182 <<
"--reachability-slice and --reachability-slice-fb must not be "
217 if(
cmdline.
isset(
"symex-complexity-failed-child-loops-limit"))
219 "symex-complexity-failed-child-loops-limit",
241 options.
set_option(
"drop-unused-functions",
true);
244 options.
set_option(
"string-abstraction",
true);
247 options.
set_option(
"reachability-slice-fb",
true);
250 options.
set_option(
"reachability-slice",
true);
299 "self-loops-to-assumptions",
320 options.
set_option(
"unwinding-assertions",
true);
321 options.
set_option(
"paths-symex-explore-all",
true);
352 options.
set_option(
"refine-arithmetic",
true);
359 options.
set_option(
"refine-arithmetic",
true);
370 "max-node-refinement",
386 if(
cmdline.
isset(
"ignore-properties-before-unwind-min"))
387 options.
set_option(
"ignore-properties-before-unwind-min",
true);
391 log.
error() <<
"--paths not supported with --incremental-loop"
411 bool solver_set=
false;
415 options.
set_option(
"boolector",
true), solver_set=
true;
421 options.
set_option(
"cprover-smt2",
true), solver_set =
true;
427 options.
set_option(
"mathsat",
true), solver_set=
true;
433 options.
set_option(
"cvc4",
true), solver_set=
true;
439 options.
set_option(
"yices",
true), solver_set=
true;
445 options.
set_option(
"z3",
true), solver_set=
true;
467 options.
set_option(
"sat-preprocessor",
false);
485 "symex-coverage-report",
487 options.
set_option(
"paths-symex-explore-all",
true);
492 options.
set_option(
"validate-ssa-equation",
true);
497 options.
set_option(
"validate-goto-model",
true);
501 options.
set_option(
"show-goto-symex-steps",
true);
539 log.
error() <<
"This version of CBMC has no support for "
540 " hardware modules. Please use hw-cbmc."
551 gcc_version.
get(
"gcc");
579 std::ifstream infile(
widen(filename));
581 std::ifstream infile(filename);
586 log.
error() <<
"failed to open input file '" << filename <<
"'"
591 std::unique_ptr<languaget> language=
594 if(language==
nullptr)
596 log.
error() <<
"failed to figure out type of file '" << filename <<
"'"
606 if(language->
parse(infile, filename))
616 int get_goto_program_ret =
619 if(get_goto_program_ret!=-1)
620 return get_goto_program_ret;
671 if(options.
is_set(
"cover"))
684 std::unique_ptr<goto_verifiert> verifier =
nullptr;
686 if(options.
is_set(
"incremental-loop"))
705 util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
721 util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
755 const resultt result = (*verifier)();
833 std::ifstream infile(filename);
844 if(language ==
nullptr)
852 if(language->
preprocess(infile, filename, std::cout))
877 log.
status() <<
"Removal of function pointers and virtual functions"
906 log.
status() <<
"Adding nondeterministic initialization "
907 "of static/global variables"
940 if(options.
is_set(
"cover"))
959 log.
status() <<
"Performing a forwards-backwards reachability slice"
961 if(options.
is_set(
"property"))
971 if(options.
is_set(
"property"))
981 if(options.
is_set(
"property"))
1007 " cbmc [-?] [-h] [--help] show help\n"
1008 " cbmc file.c ... source file names\n"
1010 "Analysis options:\n"
1012 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n"
1013 " --property id only check one specific property\n"
1014 " --stop-on-fail stop analysis once a failed property is detected\n"
1015 " --trace give a counterexample trace for failed properties\n"
1017 "C/C++ frontend options:\n"
1018 " -I path set include path (C/C++)\n"
1019 " -D macro define preprocessor macro (C/C++)\n"
1020 " --preprocess stop after preprocessing\n"
1021 " --16, --32, --64 set width of int\n"
1022 " --LP64, --ILP64, --LLP64,\n"
1023 " --ILP32, --LP32 set width of int, long and pointers\n"
1024 " --little-endian allow little-endian word-byte conversions\n"
1025 " --big-endian allow big-endian word-byte conversions\n"
1026 " --unsigned-char make \"char\" unsigned by default\n"
1027 " --mm model set memory model (default: sc)\n"
1028 " --arch set architecture (default: "
1030 " --os set operating system (default: "
1032 " --c89/99/11 set C language standard (default: "
1039 " --cpp98/03/11 set C++ language standard (default: "
1047 " --gcc use GCC as preprocessor\n"
1049 " --no-arch don't set up an architecture\n"
1050 " --no-library disable built-in abstract C library\n"
1051 " --round-to-nearest rounding towards nearest even (default)\n"
1052 " --round-to-plus-inf rounding towards plus infinity\n"
1053 " --round-to-minus-inf rounding towards minus infinity\n"
1054 " --round-to-zero rounding towards zero\n"
1058 "Program representations:\n"
1059 " --show-parse-tree show parse tree\n"
1060 " --show-symbol-table show loaded symbol table\n"
1063 "Program instrumentation options:\n"
1065 " --no-assertions ignore user assertions\n"
1066 " --no-assumptions ignore user assumptions\n"
1067 " --error-label label check that label is unreachable\n"
1068 " --cover CC create test-suite with coverage criterion CC\n"
1069 " --mm MM memory consistency model for concurrent programs\n"
1072 " --full-slice run full slicer (experimental)\n"
1073 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1075 "Semantic transformations:\n"
1077 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1082 "Backend options:\n"
1083 " --object-bits n number of bits used for object addresses\n"
1084 " --dimacs generate CNF in DIMACS format\n"
1085 " --beautify beautify the counterexample (greedy heuristic)\n"
1086 " --localize-faults localize faults (experimental)\n"
1087 " --smt2 use default SMT2 solver (Z3)\n"
1088 " --boolector use Boolector\n"
1089 " --cprover-smt2 use CPROVER SMT2 solver\n"
1090 " --cvc4 use CVC4\n"
1091 " --mathsat use MathSAT\n"
1092 " --yices use Yices\n"
1094 " --refine use refinement procedure (experimental)\n"
1096 " --outfile filename output formula to given file\n"
1097 " --arrays-uf-never never turn arrays into uninterpreted functions\n"
1098 " --arrays-uf-always always turn arrays into uninterpreted functions\n"
1101 " --version show version and exit\n"
1107 " --verbosity # verbosity level\n"
Class that provides messages with a built-in verbosity 'level'.
const char * CBMC_VERSION
virtual int doit() override
invoke main modules
#define UNREACHABLE
This should be used to mark dead code.
#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
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
mstreamt & status() const
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
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)
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
void set_option(const std::string &option, const bool value)
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
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)
#define HELP_REACHABILITY_SLICER_FB
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 instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler)
Applies instrumenters to given goto program.
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()
static void remove_vector(typet &)
removes vector data type
std::unique_ptr< T > util_make_unique(Ts &&... ts)
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.
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the sta...
std::string banner_string(const std::string &front_end, const std::string &version)
void get_command_line_options(optionst &)
preprocessort preprocessor
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
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)
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.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
virtual void set_message_handler(message_handlert &_message_handler)
#define HELP_SHOW_PROPERTIES
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
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)
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.
void compute_loop_numbers()
#define HELP_STRING_REFINEMENT_CBMC
std::wstring widen(const char *s)
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
static c_standardt default_c_standard()
#define HELP_ANSI_C_LANGUAGE
static void remove_complex(typet &)
removes complex data type
virtual void report()=0
Report results.
static irep_idt this_architecture()
message_handlert & get_message_handler()
int result_to_exit_code(resultt result)
goto_functionst goto_functions
GOTO functions.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
bool set(const cmdlinet &cmdline)
static cpp_standardt default_cpp_standard()
bool get_bool_option(const std::string &option) const
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
#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)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
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.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
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.
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)