71 ui_message_handler(cmdline,
"CBMC " CBMC_VERSION),
72 path_strategy_chooser()
79 const std::string &extra_options):
83 ui_message_handler(cmdline,
"CBMC " CBMC_VERSION),
84 path_strategy_chooser()
93 options.
set_option(
"built-in-assertions",
true);
116 error() <<
"--cover and --unwinding-assertions must not be given together" 123 error() <<
"--partial-loops and --unwinding-assertions must not be given " 124 <<
"together" <<
eom;
131 error() <<
"--reachability-slice and --reachability-slice-fb must not be " 132 <<
"given together" <<
eom;
178 options.
set_option(
"drop-unused-functions",
true);
181 options.
set_option(
"string-abstraction",
true);
184 options.
set_option(
"reachability-slice-fb",
true);
187 options.
set_option(
"reachability-slice",
true);
209 "localize-faults-method",
234 "self-loops-to-assumptions",
254 options.
set_option(
"unwinding-assertions",
true);
284 options.
set_option(
"refine-arithmetic",
true);
291 options.
set_option(
"refine-arithmetic",
true);
305 "max-node-refinement",
315 error() <<
"--smt1 is no longer supported" <<
eom;
325 bool solver_set=
false;
329 options.
set_option(
"boolector",
true), solver_set=
true;
335 options.
set_option(
"mathsat",
true), solver_set=
true;
341 options.
set_option(
"cvc4",
true), solver_set=
true;
347 options.
set_option(
"yices",
true), solver_set=
true;
353 options.
set_option(
"z3",
true), solver_set=
true;
375 options.
set_option(
"sat-preprocessor",
false);
392 "symex-coverage-report",
403 std::cout << CBMC_VERSION <<
'\n';
417 catch(
const char *error_msg)
423 catch(
const std::string &error_msg)
435 status() <<
"CBMC version " CBMC_VERSION
" " 436 <<
sizeof(
void *)*8 <<
"-bit " 447 error() <<
"This version of CBMC has no support for " 448 " hardware modules. Please use hw-cbmc." <<
eom;
470 error() <<
"Please give exactly one source file" <<
eom;
477 std::ifstream infile(
widen(filename));
479 std::ifstream infile(filename);
484 error() <<
"failed to open input file `" 485 << filename <<
"'" <<
eom;
489 std::unique_ptr<languaget> language=
492 if(language==
nullptr)
494 error() <<
"failed to figure out type of file `" 495 << filename <<
"'" <<
eom;
502 status() <<
"Parsing " << filename <<
eom;
504 if(language->
parse(infile, filename))
514 int get_goto_program_ret =
517 if(get_goto_program_ret!=-1)
518 return get_goto_program_ret;
556 catch(
const std::string &e)
564 error() <<
"Numeric exception : " << e <<
eom;
580 log.
error() <<
"Please provide a program to verify" << log.
eom;
626 catch(
const std::string &e)
634 log.
error() <<
"Numeric exception : " << e << log.
eom;
638 catch(
const std::bad_alloc &)
640 log.
error() <<
"Out of memory" << log.
eom;
653 error() <<
"Please provide one program to preprocess" <<
eom;
659 std::ifstream infile(filename);
663 error() <<
"failed to open input file" <<
eom;
670 if(language==
nullptr)
672 error() <<
"failed to figure out type of file" <<
eom;
678 if(language->
preprocess(infile, filename, std::cout))
679 error() <<
"PREPROCESSING ERROR" <<
eom;
687 catch(
const std::string &e)
694 error() <<
"Numeric exception : " << e <<
eom;
697 catch(
const std::bad_alloc &)
727 log.
status() <<
"Removal of function pointers and virtual functions" <<
eom;
745 log.
status() <<
"Generic Property Instrumentation" <<
eom;
755 log.
status() <<
"Adding nondeterministic initialization " 756 "of static/global variables" 763 log.
status() <<
"String Abstraction" <<
eom;
780 log.
status() <<
"Removing unused functions" <<
eom;
789 if(options.
is_set(
"cover"))
805 log.
status() <<
"Performing a forwards-backwards reachability slice" 807 if(options.
is_set(
"property"))
816 log.
status() <<
"Performing a reachability slice" <<
eom;
817 if(options.
is_set(
"property"))
826 log.
status() <<
"Performing a full slice" <<
eom;
827 if(options.
is_set(
"property"))
843 catch(
const std::string &e)
851 log.
error() <<
"Numeric exception : " << e <<
eom;
855 catch(
const std::bad_alloc &)
857 log.
error() <<
"Out of memory" <<
eom;
869 std::cout <<
'\n' <<
banner_string(
"CBMC", CBMC_VERSION) <<
'\n' 871 "* * Copyright (C) 2001-2018 * *\n" 872 "* * Daniel Kroening, Edmund Clarke * *\n" 873 "* * Carnegie Mellon University, Computer Science Department * *\n" 874 "* * kroening@kroening.com * *\n" 875 "* * Protected in part by U.S. patent 7,225,417 * *\n" 879 " cbmc [-?] [-h] [--help] show help\n" 880 " cbmc file.c ... source file names\n" 882 "Analysis options:\n" 884 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" 885 " --property id only check one specific property\n" 886 " --stop-on-fail stop analysis once a failed property is detected\n" 887 " --trace give a counterexample trace for failed properties\n" 889 "C/C++ frontend options:\n" 890 " -I path set include path (C/C++)\n" 891 " -D macro define preprocessor macro (C/C++)\n" 892 " --preprocess stop after preprocessing\n" 893 " --16, --32, --64 set width of int\n" 894 " --LP64, --ILP64, --LLP64,\n" 895 " --ILP32, --LP32 set width of int, long and pointers\n" 896 " --little-endian allow little-endian word-byte conversions\n" 897 " --big-endian allow big-endian word-byte conversions\n" 898 " --unsigned-char make \"char\" unsigned by default\n" 899 " --mm model set memory model (default: sc)\n" 900 " --arch set architecture (default: " 902 " --os set operating system (default: " 904 " --c89/99/11 set C language standard (default: " 911 " --cpp98/03/11 set C++ language standard (default: " 919 " --gcc use GCC as preprocessor\n" 921 " --no-arch don't set up an architecture\n" 922 " --no-library disable built-in abstract C library\n" 923 " --round-to-nearest rounding towards nearest even (default)\n" 924 " --round-to-plus-inf rounding towards plus infinity\n" 925 " --round-to-minus-inf rounding towards minus infinity\n" 926 " --round-to-zero rounding towards zero\n" 929 "Program representations:\n" 930 " --show-parse-tree show parse tree\n" 931 " --show-symbol-table show loaded symbol table\n" 933 " --drop-unused-functions drop functions trivially unreachable from main function\n" 935 "Program instrumentation options:\n" 937 " --no-assertions ignore user assertions\n" 938 " --no-assumptions ignore user assumptions\n" 939 " --error-label label check that label is unreachable\n" 940 " --cover CC create test-suite with coverage criterion CC\n" 941 " --mm MM memory consistency model for concurrent programs\n" 943 " --full-slice run full slicer (experimental)\n" 945 "Semantic transformations:\n" 947 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 953 " --object-bits n number of bits used for object addresses\n" 954 " --dimacs generate CNF in DIMACS format\n" 955 " --beautify beautify the counterexample (greedy heuristic)\n" 956 " --localize-faults localize faults (experimental)\n" 957 " --smt1 use default SMT1 solver (obsolete)\n" 958 " --smt2 use default SMT2 solver (Z3)\n" 959 " --boolector use Boolector\n" 960 " --mathsat use MathSAT\n" 962 " --yices use Yices\n" 964 " --refine use refinement procedure (experimental)\n" 965 " --refine-strings use string refinement (experimental)\n" 966 " --string-printable add constraint that strings are printable (experimental)\n" 967 " --string-max-input-length add constraint on the length of input strings\n" 968 " --string-max-length add constraint on the length of strings" 969 " (deprecated: use string-max-input-length instead)\n" 970 " --outfile filename output formula to given file\n" 971 " --arrays-uf-never never turn arrays into uninterpreted functions\n" 972 " --arrays-uf-always always turn arrays into uninterpreted functions\n" 975 " --version show version and exit\n" 976 " --xml-ui use XML-formatted output\n" 977 " --xml-interface bi-directional XML interface\n" 978 " --json-ui use JSON-formatted output\n" 981 " --verbosity # verbosity level\n"
const std::list< std::string > & get_values(const std::string &option) const
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)
struct configt::ansi_ct ansi_c
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 string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
#define HELP_REACHABILITY_SLICER
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
void get_command_line_options(optionst &)
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, messaget &, ui_message_handlert &)
Remove Indirect Function Calls.
std::wstring widen(const char *s)
virtual void get_language_options(const cmdlinet &)
std::string object_bits_info()
void compute_loop_numbers()
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...
bool is_goto_binary(const std::string &filename)
Remove the 'complex' data type by compilation into structs.
std::string get_value(char option) const
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
const value_listt & get_list_option(const std::string &option) const
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
symbol_tablet symbol_table
Symbol table.
static mstreamt & eom(mstreamt &m)
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Remove 'asm' statements by compiling into suitable standard code.
const path_strategy_choosert path_strategy_chooser
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand)...
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Set the properties to check.
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
bool set(const cmdlinet &cmdline)
Perform Memory-mapped I/O instrumentation.
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
std::string show_strategies() const
suitable for displaying as a front-end help message
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
virtual bool isset(char option) const
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
Initialize a Goto Program.
#define HELP_SHOW_PROPERTIES
Nondeterministic initialization of certain global scope variables.
bool get_bool_option(const std::string &option) const
Abstract interface to support a programming language.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
virtual void set_message_handler(message_handlert &_message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
CBMC Command Line Option Processing.
std::string banner_string(const std::string &front_end, const std::string &version)
void instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler)
Applies instrumenters to given goto program.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
virtual int doit() override
invoke main modules
static c_standardt default_c_standard()
bool test_c_preprocessor(message_handlert &message_handler)
virtual void show_parse(std::ostream &out)=0
static irep_idt this_operating_system()
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
static void set_default_options(optionst &)
Set the options that have default values.
message_handlert & get_message_handler()
Goto Programs with Functions.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
#define HELP_SHOW_GOTO_FUNCTIONS
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...
cbmc_parse_optionst(int argc, const char **argv)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
goto_modelt initialize_goto_model(const cmdlinet &cmdline, message_handlert &message_handler)
Remove the 'vector' data type by compilation into arrays.
virtual void usage_error()
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
Coverage Instrumentation.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files...
void set_option(const std::string &option, const bool value)
static void remove_complex(typet &)
removes complex data type
ui_message_handlert ui_message_handler
virtual bool parse(std::istream &instream, const std::string &path)=0
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
static cpp_standardt default_cpp_standard()
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
virtual void help() override
display command line help
void remove_asm(goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table)
removes assembler
void register_languages()
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)