71 path_strategy_chooser()
78 const std::string &extra_options)
83 path_strategy_chooser()
92 options.
set_option(
"built-in-assertions",
true);
119 error() <<
"--cover and --unwinding-assertions must not be given together" 126 error() <<
"--partial-loops and --unwinding-assertions must not be given " 127 <<
"together" <<
eom;
134 error() <<
"--reachability-slice and --reachability-slice-fb must not be " 135 <<
"given together" <<
eom;
184 options.
set_option(
"drop-unused-functions",
true);
187 options.
set_option(
"string-abstraction",
true);
190 options.
set_option(
"reachability-slice-fb",
true);
193 options.
set_option(
"reachability-slice",
true);
218 "localize-faults-method",
243 "self-loops-to-assumptions",
263 options.
set_option(
"unwinding-assertions",
true);
293 options.
set_option(
"refine-arithmetic",
true);
300 options.
set_option(
"refine-arithmetic",
true);
311 "max-node-refinement",
318 error() <<
"--smt1 is no longer supported" <<
eom;
328 bool solver_set=
false;
332 options.
set_option(
"boolector",
true), solver_set=
true;
338 options.
set_option(
"cprover-smt2",
true), solver_set =
true;
344 options.
set_option(
"mathsat",
true), solver_set=
true;
350 options.
set_option(
"cvc4",
true), solver_set=
true;
356 options.
set_option(
"yices",
true), solver_set=
true;
362 options.
set_option(
"z3",
true), solver_set=
true;
384 options.
set_option(
"sat-preprocessor",
false);
401 "symex-coverage-report",
406 options.
set_option(
"validate-ssa-equation",
true);
411 options.
set_option(
"validate-goto-model",
true);
436 catch(
const char *error_msg)
442 catch(
const std::string &error_msg)
465 error() <<
"This version of CBMC has no support for " 466 " hardware modules. Please use hw-cbmc." <<
eom;
488 error() <<
"Please give exactly one source file" <<
eom;
495 std::ifstream infile(
widen(filename));
497 std::ifstream infile(filename);
502 error() <<
"failed to open input file `" 503 << filename <<
"'" <<
eom;
507 std::unique_ptr<languaget> language=
510 if(language==
nullptr)
512 error() <<
"failed to figure out type of file `" 513 << filename <<
"'" <<
eom;
520 status() <<
"Parsing " << filename <<
eom;
522 if(language->
parse(infile, filename))
532 int get_goto_program_ret =
535 if(get_goto_program_ret!=-1)
536 return get_goto_program_ret;
575 catch(
const std::string &e)
583 error() <<
"Numeric exception : " << e <<
eom;
599 log.
error() <<
"Please provide a program to verify" << log.
eom;
652 catch(
const std::string &e)
660 log.
error() <<
"Numeric exception : " << e << log.
eom;
664 catch(
const std::bad_alloc &)
666 log.
error() <<
"Out of memory" << log.
eom;
679 error() <<
"Please provide one program to preprocess" <<
eom;
685 std::ifstream infile(filename);
689 error() <<
"failed to open input file" <<
eom;
696 if(language==
nullptr)
698 error() <<
"failed to figure out type of file" <<
eom;
704 if(language->
preprocess(infile, filename, std::cout))
705 error() <<
"PREPROCESSING ERROR" <<
eom;
713 catch(
const std::string &e)
720 error() <<
"Numeric exception : " << e <<
eom;
723 catch(
const std::bad_alloc &)
753 log.
status() <<
"Removal of function pointers and virtual functions" <<
eom;
771 log.
status() <<
"Generic Property Instrumentation" <<
eom;
781 log.
status() <<
"Adding nondeterministic initialization " 782 "of static/global variables" 789 log.
status() <<
"String Abstraction" <<
eom;
806 log.
status() <<
"Removing unused functions" <<
eom;
815 if(options.
is_set(
"cover"))
831 log.
status() <<
"Performing a forwards-backwards reachability slice" 833 if(options.
is_set(
"property"))
842 log.
status() <<
"Performing a reachability slice" <<
eom;
843 if(options.
is_set(
"property"))
852 log.
status() <<
"Performing a full slice" <<
eom;
853 if(options.
is_set(
"property"))
869 catch(
const std::string &e)
877 log.
error() <<
"Numeric exception : " << e <<
eom;
881 catch(
const std::bad_alloc &)
883 log.
error() <<
"Out of memory" <<
eom;
897 "* * Copyright (C) 2001-2018 * *\n" 898 "* * Daniel Kroening, Edmund Clarke * *\n" 899 "* * Carnegie Mellon University, Computer Science Department * *\n" 900 "* * kroening@kroening.com * *\n" 901 "* * Protected in part by U.S. patent 7,225,417 * *\n" 905 " cbmc [-?] [-h] [--help] show help\n" 906 " cbmc file.c ... source file names\n" 908 "Analysis options:\n" 910 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" 911 " --property id only check one specific property\n" 912 " --stop-on-fail stop analysis once a failed property is detected\n" 913 " --trace give a counterexample trace for failed properties\n" 915 "C/C++ frontend options:\n" 916 " -I path set include path (C/C++)\n" 917 " -D macro define preprocessor macro (C/C++)\n" 918 " --preprocess stop after preprocessing\n" 919 " --16, --32, --64 set width of int\n" 920 " --LP64, --ILP64, --LLP64,\n" 921 " --ILP32, --LP32 set width of int, long and pointers\n" 922 " --little-endian allow little-endian word-byte conversions\n" 923 " --big-endian allow big-endian word-byte conversions\n" 924 " --unsigned-char make \"char\" unsigned by default\n" 925 " --mm model set memory model (default: sc)\n" 926 " --arch set architecture (default: " 928 " --os set operating system (default: " 930 " --c89/99/11 set C language standard (default: " 937 " --cpp98/03/11 set C++ language standard (default: " 945 " --gcc use GCC as preprocessor\n" 947 " --no-arch don't set up an architecture\n" 948 " --no-library disable built-in abstract C library\n" 949 " --round-to-nearest rounding towards nearest even (default)\n" 950 " --round-to-plus-inf rounding towards plus infinity\n" 951 " --round-to-minus-inf rounding towards minus infinity\n" 952 " --round-to-zero rounding towards zero\n" 956 "Program representations:\n" 957 " --show-parse-tree show parse tree\n" 958 " --show-symbol-table show loaded symbol table\n" 961 "Program instrumentation options:\n" 963 " --no-assertions ignore user assertions\n" 964 " --no-assumptions ignore user assumptions\n" 965 " --error-label label check that label is unreachable\n" 966 " --cover CC create test-suite with coverage criterion CC\n" 967 " --mm MM memory consistency model for concurrent programs\n" 970 " --full-slice run full slicer (experimental)\n" 971 " --drop-unused-functions drop functions trivially unreachable from main function\n" 973 "Semantic transformations:\n" 975 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 981 " --object-bits n number of bits used for object addresses\n" 982 " --dimacs generate CNF in DIMACS format\n" 983 " --beautify beautify the counterexample (greedy heuristic)\n" 984 " --localize-faults localize faults (experimental)\n" 985 " --smt2 use default SMT2 solver (Z3)\n" 986 " --boolector use Boolector\n" 987 " --cprover-smt2 use CPROVER SMT2 solver\n" 989 " --mathsat use MathSAT\n" 990 " --yices use Yices\n" 992 " --refine use refinement procedure (experimental)\n" 994 " --outfile filename output formula to given file\n" 995 " --arrays-uf-never never turn arrays into uninterpreted functions\n" 996 " --arrays-uf-always always turn arrays into uninterpreted functions\n" 999 " --version show version and exit\n" 1000 " --xml-ui use XML-formatted output\n" 1001 " --xml-interface bi-directional XML interface\n" 1002 " --json-ui use JSON-formatted output\n" 1007 " --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)
std::string object_bits_info()
void compute_loop_numbers()
#define HELP_ANSI_C_LANGUAGE
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.
#define HELP_REACHABILITY_SLICER_FB
std::string get_value(char option) const
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
#define HELP_STRING_REFINEMENT_CBMC
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.
#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 them into suitable standard goto program instructions.
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)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
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)
void preprocessing(const optionst &)
Perform Memory-mapped I/O instrumentation.
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
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Nondeterministically initializes global scope variables, except for constants (such as string literal...
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 cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Class that provides messages with a built-in verbosity 'level'.
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.
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...
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 int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, 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)...
static void set_default_options(optionst &)
Set the options that have default values.
message_handlert & get_message_handler()
Document and give macros for the exit codes of CPROVER binaries.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
mstreamt & status() const
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
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 std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
virtual void set_language_options(const optionst &)
Set language-specific options.
Remove the 'vector' data type by compilation into arrays.
std::string what() const override
A human readable description of what went wrong.
virtual void usage_error()
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)
Nondeterministically initializes global scope variables in a goto-function.
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
virtual void help() override
display command line help
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)