78 const std::string &extra_options):
160 "localize-faults-method",
190 options.
set_option(
"java-unwind-enum-static",
true);
210 options.
set_option(
"unwinding-assertions",
false);
214 "unwinding-assertions",
226 error() <<
"--partial-loops and --unwinding-assertions " 227 <<
"must not be given together" <<
eom;
261 options.
set_option(
"refine-arithmetic",
true);
268 options.
set_option(
"refine-arithmetic",
true);
273 "max-node-refinement",
280 bool version_set=
false;
301 bool solver_set=
false;
305 options.
set_option(
"boolector",
true), solver_set=
true;
307 options.
set_option(
"smt2",
true), version_set=
true;
312 options.
set_option(
"mathsat",
true), solver_set=
true;
314 options.
set_option(
"smt2",
true), version_set=
true;
319 options.
set_option(
"cvc3",
true), solver_set=
true;
321 options.
set_option(
"smt1",
true), version_set=
true;
326 options.
set_option(
"cvc4",
true), solver_set=
true;
328 options.
set_option(
"smt2",
true), version_set=
true;
333 options.
set_option(
"yices",
true), solver_set=
true;
335 options.
set_option(
"smt2",
true), version_set=
true;
340 options.
set_option(
"z3",
true), solver_set=
true;
342 options.
set_option(
"smt2",
true), version_set=
true;
347 options.
set_option(
"opensmt",
true), solver_set=
true;
349 options.
set_option(
"smt1",
true), version_set=
true;
352 if(version_set && !solver_set)
357 options.
set_option(
"generic",
true), solver_set=
true;
363 options.
set_option(
"boolector",
true), solver_set=
true;
368 options.
set_option(
"z3",
true), solver_set=
true;
373 assert(version_set==solver_set);
379 options.
set_option(
"sat-preprocessor",
false);
399 "symex-coverage-report",
424 <<
sizeof(
void *)*8 <<
"-bit " 435 error() <<
"This version of CBMC has no support for " 436 " hardware modules. Please use hw-cbmc." <<
eom;
455 int get_goto_program_ret=
458 if(get_goto_program_ret!=-1)
459 return get_goto_program_ret;
481 std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
488 catch(
const char *error_msg)
499 return do_bmc(bmc, goto_functions);
519 catch(
const std::string e)
540 error() <<
"Please provide a program to verify" <<
eom;
551 error() <<
"Please give exactly one source file" <<
eom;
558 std::ifstream infile(
widen(filename));
560 std::ifstream infile(filename);
565 error() <<
"failed to open input file `" 566 << filename <<
"'" <<
eom;
572 if(language==
nullptr)
574 error() <<
"failed to figure out type of file `" 575 << filename <<
"'" <<
eom;
581 status() <<
"Parsing " << filename <<
eom;
583 if(language->
parse(infile, filename))
596 for(cmdlinet::argst::iterator
603 binaries.push_back(*it);
618 if(get_modules_ret!=-1)
619 return get_modules_ret;
620 if(binaries.empty() &&
final())
627 for(
const auto &bin : binaries)
629 status() <<
"Reading GOTO program from file " <<
eom;
641 if(!binaries.empty())
650 status() <<
"Generating GOTO Program" <<
eom;
679 catch(
const std::string e)
690 catch(std::bad_alloc)
705 error() <<
"Please provide one program to preprocess" <<
eom;
711 std::ifstream infile(filename);
715 error() <<
"failed to open input file" <<
eom;
723 error() <<
"failed to figure out type of file" <<
eom;
729 std::unique_ptr<languaget> language(ptr);
731 if(language->
preprocess(infile, filename, std::cout))
732 error() <<
"PREPROCESSING ERROR" <<
eom;
740 catch(
const std::string e)
749 catch(std::bad_alloc)
775 status() <<
"Removal of function pointers and virtual functions" <<
eom;
801 status() <<
"Generic Property Instrumentation" <<
eom;
811 status() <<
"Adding nondeterministic initialization " 812 "of static/global variables" <<
eom;
838 status() <<
"Removing unused functions" <<
eom;
863 status() <<
"Performing a full slice" <<
eom;
881 catch(
const std::string e)
892 catch(std::bad_alloc)
911 switch(bmc.
run(goto_functions))
939 std::cout <<
"(" << (
sizeof(
void *)*8) <<
"-bit version)";
941 std::cout <<
" * *\n";
944 "* * Daniel Kroening, Edmund Clarke * *\n" 945 "* * Carnegie Mellon University, Computer Science Department * *\n" 946 "* * kroening@kroening.com * *\n" 947 "* * Protected in part by U.S. patent 7,225,417 * *\n" 951 " cbmc [-?] [-h] [--help] show help\n" 952 " cbmc file.c ... source file names\n" 954 "Analysis options:\n" 955 " --show-properties show the properties, but don't run analysis\n" 956 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" 957 " --property id only check one specific property\n" 958 " --stop-on-fail stop analysis once a failed property is detected\n" 959 " --trace give a counterexample trace for failed properties\n" 961 "C/C++ frontend options:\n" 962 " -I path set include path (C/C++)\n" 963 " -D macro define preprocessor macro (C/C++)\n" 964 " --preprocess stop after preprocessing\n" 965 " --16, --32, --64 set width of int\n" 966 " --LP64, --ILP64, --LLP64,\n" 967 " --ILP32, --LP32 set width of int, long and pointers\n" 968 " --little-endian allow little-endian word-byte conversions\n" 969 " --big-endian allow big-endian word-byte conversions\n" 970 " --unsigned-char make \"char\" unsigned by default\n" 971 " --mm model set memory model (default: sc)\n" 972 " --arch set architecture (default: " 974 " --os set operating system (default: " 976 " --c89/99/11 set C language standard (default: " 983 " --cpp98/03/11 set C++ language standard (default: " 991 " --gcc use GCC as preprocessor\n" 993 " --no-arch don't set up an architecture\n" 994 " --no-library disable built-in abstract C library\n" 995 " --round-to-nearest rounding towards nearest even (default)\n" 996 " --round-to-plus-inf rounding towards plus infinity\n" 997 " --round-to-minus-inf rounding towards minus infinity\n" 998 " --round-to-zero rounding towards zero\n" 999 " --function name set main function name\n" 1001 "Program representations:\n" 1002 " --show-parse-tree show parse tree\n" 1003 " --show-symbol-table show symbol table\n" 1005 " --drop-unused-functions drop functions trivially unreachable from main function\n" 1007 "Program instrumentation options:\n" 1009 " --no-assertions ignore user assertions\n" 1010 " --no-assumptions ignore user assumptions\n" 1011 " --error-label label check that label is unreachable\n" 1012 " --cover CC create test-suite with coverage criterion CC\n" 1013 " --mm MM memory consistency model for concurrent programs\n" 1015 "Java Bytecode frontend options:\n" 1016 " --classpath dir/jar set the classpath\n" 1017 " --main-class class-name set the name of the main class\n" 1019 " --java-max-vla-length limit the length of user-code-created arrays\n" 1021 " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" 1022 " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" 1024 "Semantic transformations:\n" 1025 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 1028 " --program-only only show program expression\n" 1029 " --show-loops show the loops in the program\n" 1030 " --depth nr limit search depth\n" 1031 " --unwind nr unwind nr times\n" 1032 " --unwindset L:B,... unwind loop L with a bound of B\n" 1033 " (use --show-loops to get the loop IDs)\n" 1034 " --show-vcc show the verification conditions\n" 1035 " --slice-formula remove assignments unrelated to property\n" 1036 " --unwinding-assertions generate unwinding assertions\n" 1037 " --partial-loops permit paths with partial loops\n" 1038 " --no-pretty-names do not simplify identifiers\n" 1039 " --graphml-witness filename write the witness in GraphML format to filename\n" 1041 "Backend options:\n" 1042 " --dimacs generate CNF in DIMACS format\n" 1043 " --beautify beautify the counterexample (greedy heuristic)\n" 1044 " --localize-faults localize faults (experimental)\n" 1045 " --smt1 use default SMT1 solver (obsolete)\n" 1046 " --smt2 use default SMT2 solver (Z3)\n" 1047 " --boolector use Boolector\n" 1048 " --mathsat use MathSAT\n" 1049 " --cvc4 use CVC4\n" 1050 " --yices use Yices\n" 1052 " --refine use refinement procedure (experimental)\n" 1053 " --outfile filename output formula to given file\n" 1054 " --arrays-uf-never never turn arrays into uninterpreted functions\n" 1055 " --arrays-uf-always always turn arrays into uninterpreted functions\n" 1058 " --version show version and exit\n" 1059 " --xml-ui use XML-formatted output\n" 1060 " --xml-interface bi-directional XML interface\n" 1061 " --json-ui use JSON-formatted output\n" 1062 " --verbosity # verbosity level\n"
symbol_tablet symbol_table
const std::list< std::string > & get_values(const std::string &option) const
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
struct configt::ansi_ct ansi_c
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
Remove function exceptional returns.
Remove Instance-of Operators.
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Remove Indirect Function Calls.
std::wstring widen(const char *s)
Remove Virtual Function (Method) Calls.
void remove_unused_functions(goto_functionst &functions, message_handlert &message_handler)
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
bool set_properties(goto_functionst &goto_functions)
unsigned unsafe_string2unsigned(const std::string &str, int base)
void remove_static_init_loops(const symbol_tablet &symbol_table, const goto_functionst &goto_functions, optionst &options)
this is the entry point for the removal of loops in static initialization code of Java enums ...
bool is_goto_binary(const std::string &filename)
Remove the 'complex' data type by compilation into structs.
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
std::string get_value(char option) const
prop_convt & prop_conv() const
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
virtual void show_symbol_table(bool brief=false)
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
static mstreamt & eom(mstreamt &m)
Remove 'asm' statements by compiling into suitable standard code.
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void remove_virtual_functions(const symbol_tablet &symbol_table, goto_functionst &goto_functions)
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Set the properties to check.
void compute_loop_numbers()
bool set(const cmdlinet &cmdline)
virtual void get_command_line_options(optionst &options)
virtual int do_bmc(bmct &bmc, const goto_functionst &goto_functions)
invoke main modules
Perform Memory-mapped I/O instrumentation.
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
virtual bool isset(char option) const
virtual std::unique_ptr< solvert > get_solver()
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
virtual bool process_goto_program(const optionst &options, goto_functionst &goto_functions)
void set_ui(language_uit::uit _ui)
virtual int get_modules(expr_listt &bmc_constraints)
Nondeterministic initialization of certain global scope variables.
void instrument_cover_goals(const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont criterion)
bool get_bool_option(const std::string &option) const
static mstreamt & endl(mstreamt &m)
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 resultt run(const goto_functionst &goto_functions)
void set_ui(language_uit::uit _ui)
virtual void set_message_handler(message_handlert &_message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
std::vector< std::string > argst
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.
bool read_object_and_link(const std::string &file_name, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads an object file
std::list< exprt > expr_listt
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void set_from_symbol_table(const symbol_tablet &)
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
virtual int get_goto_program(const optionst &options, expr_listt &bmc_constraints, goto_functionst &goto_functions)
virtual void clear_parse()
static irep_idt this_operating_system()
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
message_handlert & get_message_handler()
Bounded Model Checking for ANSI-C + HDL.
Goto Programs with Functions.
#define HELP_SHOW_GOTO_FUNCTIONS
languaget * get_language_from_filename(const std::string &filename)
cbmc_parse_optionst(int argc, const char **argv)
void memory_info(std::ostream &out)
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Bounded Model Checking for ANSI-C + HDL.
Remove the 'vector' data type by compilation into arrays.
void set_verbosity(unsigned _verbosity)
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.
void set_option(const std::string &option, const bool value)
void add_failed_symbols(symbol_tablet &symbol_table)
static void remove_complex(typet &)
removes complex data type
ui_message_handlert ui_message_handler
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
virtual bool parse(std::istream &instream, const std::string &path)=0
static cpp_standardt default_cpp_standard()
Unwind loops in static initializers.
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
void label_properties(goto_modelt &goto_model)
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)
virtual void help() override
display command line help
virtual void register_languages()