Provided by: cbmc_5.3-1_amd64
cbmc - Bounded Model Checker for C/C++ and Java programs
cbmc [--property property-id] file.c ... cbmc [--show-properties] file.c ... cbmc [--all-properties] file.c ... goto-cc [-I include-path] [-c] file.c [-o outfile.o] goto-instrument infile outfile Only the most useful options are listed here; see below for the remainder.
cbmc generates traces that demonstrate how an assertion can be violated, or proves that the assertion cannot be violated within a given number of loop iterations. CBMC can read source-code directly, or a goto-binary generated by goto-cc. Java programs are given as class files. Without any further options, cbmc checks all properties (automatically generated or user-specified) found in the program. If any of the properties can be violated, a counterexample is printed and the analysis is aborted. The analysis can be restricted to a particular property with the --property option. The verification result for all properties can be obtained by means of the --all-properties option. goto-cc reads source code, and generates a goto-binary. Its command-line interface is designed to mimic that of gcc(1). Note in particular that goto-cc distinguishes between compiling and linking phases, just as gcc does. cbmc expects a goto-binary for which linking has been completed. goto-instrument reads a goto-binary, performs a given program transformation, and then writes the resulting program as goto-binary on disc. The usual flow is to (1) translate source into a goto-binary using goto-cc, then (2) perform instrumentation with goto-instrument, and finally (3) perform the analysis with cbmc.
FRONTEND OPTIONS (cbmc and goto-cc) -I path Set include path (C/C++) -D macro Define preprocessor macro (C/C++) --preprocess Stop after preprocessing --show-symbol-table Show symbol table --show-goto-functions Show goto program ARCHITECTURAL OPTIONS (cbmc and goto-cc) cbmc by default uses architectural settings that match those of the machine cbmc is executed on, i.e., the settings below are only needed when verifying software that is meant to run on a different architecture or OS. goto-cc generates a goto-binary for a particular architecture, i.e., the architecture cannot be changed after the goto-binary is generated. --16, --32, --64 Set width of int --LP64, --ILP64, --LLP64, --ILP32, --LP32 Set width of int, long and pointers --little-endian Allow little-endian word-byte conversions --big-endian Allow big-endian word-byte conversions --unsigned-char Make "char" unsigned by default --arch Set target architecture --os Set target operating system --no-arch Don't set up an architecture --no-library Disable built-in abstract C library --round-to-nearest, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero IEEE floating point rounding mode to use when the program begins (default is round to nearest). The program under verification can override this setting, e.g., with fesetround(3). PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument) Both cbmc and goto-instrument can generate assertions that catch specific common errors, as listed below. --bounds-check Enable array bounds checks --div-by-zero-check Enable division by zero checks --pointer-check Enable pointer checks --signed-overflow-check Enable arithmetic over- and underflow checks for signed integer arithmetic --unsigned-overflow-check Enable arithmetic over- and underflow checks for unsigned integer arithmetic --nan-check Check floating-point computations for NaN --no-assertions Ignore user-provided assertions --no-assumptions Ignore user-provided assumptions --error-label label Check that the given label is unreachable PROGRAM INSTRUMENTATION OPTIONS (goto-instrument only) goto-instrument supports further, more complex, program transformations. --nondet-volatile Makes reads from volatile variables non-deterministic --isr function Instruments an interrupt service routine with the given name --mmio Instruments memory-mapped I/O --nondet-static Variables with static lifetime are initialized non-deterministically --dump-c Output ANSI-C source code instead of a goto binary. BMC OPTIONS (cbmc) --all-properties Report status of all properties --show-properties Only show properties --show-loops Show the loops in the program --cover-assertions Check which assertions are reachable --function name Set main function name --property id Only check specific property with given identifier --program-only Only show program expression --depth nr Limit search depth --unwind nr Unwind loops nr times --unwindset L:B,... Unwind loop L with a bound of B (use --show-loops to get the loop IDs) --show-vcc Show the verification conditions --slice-formula Remove assignments unrelated to property --no-unwinding-assertions Do not generate unwinding assertions --no-pretty-names Do not simplify identifiers BACKEND OPTIONS (cbmc) --dimacs Generate CNF in DIMACS format for use by external SAT solvers --beautify-greedy Beautify the counterexample (greedy heuristic) --smt1 Output subgoals in SMT1 syntax (experimental) --smt2 Output subgoals in SMT2 syntax (experimental) --boolector Use Boolector (experimental) --mathsat Use MathSAT (experimental) --cvc Use CVC3 (experimental) --yices Use Yices (experimental) --z3 Use Z3 (experimental) --refine Use refinement procedure (experimental) --outfile filename Output formula to given file --arrays-uf-never Never turn arrays into uninterpreted functions --arrays-uf-always Always turn arrays into uninterpreted functions
All tools honor the TMPDIR environment variable when generating temporary files and directories. Furthermore note that the preprocessor used by CBMC will use environment variables to locate header files. GOTO-CC aims to accept all environment variables that GCC does.
2001-2014, Daniel Kroening, Edmund Clarke