CBMC(1)

NAME
cbmc - Bounded Model Checker for C/C++ and Java programs

SYNOPSIS
cbmc [--property property-id] file.c ...

cbmc [--show-properties] file.c ...

cbmc [--all-properties] file.c ...

cbmc [--no-standard-checks] file.c ...

cbmc [--no-standard-checks] [--pointer-check] file.c ...

cbmc [--no-bounds-check] 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.

DESCRIPTION
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 C/C++ source-code directly, or a GOTO binary generated by goto-cc. Java programs are given as class or JAR 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(1) 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(1) distinguishes between compiling and linking phases, just as gcc does. cbmc expects a GOTO binary for which linking has been completed.

goto-instrument(1) 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.

OPTIONS

  Standard Checks
From version 6.0 onwards, cbmc, goto-analyzer and some other tools apply some checks to the program by default (called the "standard checks"), with the aim to provide a better user experience for a non-expert user of the tool. These checks are:

--pointer-check
    enable pointer checks

--bounds-check
    enable array bounds checks

--undefined-shift-check
    check shift greater than bit-width

--div-by-zero-check
    enable division by zero checks for integer division

--float-div-by-zero-check
    enable division by zero checks for floating-point division

--pointer-primitive-check
    checks that all pointers in pointer primitives are valid or null

--signed-overflow-check
    enable signed arithmetic over- and underflow checks

--malloc-may-fail
    allow malloc calls to return a null pointer

--malloc-fail-null
    set malloc failure mode to return null

--unwinding-assertions
    generate unwinding assertions (cannot be used with --cover)

These checks can all be deactivated at once by using the --no-standard-checks flag like in the header example, or individually, by prepending a no- before the flag, like so:

--no-pointer-check
    disable pointer checks

--no-bounds-check
    disable array bounds checks

--no-undefined-shift-check
    do not perform check for shift greater than bit-width

--no-div-by-zero-check
    disable division by zero checks

--no-pointer-primitive-check
    do not check that all pointers in pointer primitives are valid or null

--no-signed-overflow-check
    disable signed arithmetic over- and underflow checks

--no-malloc-may-fail
    do not allow malloc calls to fail by default

--no-unwinding-assertions
    do not generate unwinding assertions

If an already set flag is re-set, like calling --pointer-check when default checks are already on, the flag is simply ignored.

  Analysis options:

--no-standard-checks
    disable the standard (default) checks applied to a C/GOTO program (see above for more information)

--show-properties
    show the properties, but don't run analysis

--symex-coverage-report f
    generate a Cobertura XML coverage report in f

--property id
    only check one specific property

--trace
    give a counterexample trace for failed properties

--stop-on-fail
    stop analysis once a failed property is detected (implies --trace)

--localize-faults
    localize faults (experimental)

  C/C++ frontend options:

--preprocess
    stop after preprocessing

--test-preprocessor
    stop after preprocessing, discard output

-I path
    set include path (C/C++)

--include file
    set include file (C/C++)

-D macro
    define preprocessor macro (C/C++)

--c89, --c99, --c11, --c17, --c23
    set C language standard (default: c11)

--cpp98, --cpp03, --cpp11
    set C++ language standard (default: cpp98)

--unsigned-char
    make "char" unsigned by default

--round-to-nearest, --round-to-even
    rounding towards nearest even (default)

--round-to-plus-inf
    rounding towards plus infinity

--round-to-minus-inf
    rounding towards minus infinity

--round-to-zero
    rounding towards zero

--no-library
    disable built-in abstract C library

--max-nondet-tree-depth N
    limit size of nondet (e.g. input) object tree; at level N pointers are set to null

--min-null-tree-depth N
    minimum level at which a pointer can first be NULL in a recursively nondet initialized struct

--function name
    set main function name

  Platform options:

--arch arch
    Set analysis architecture, which defaults to the host architecture. Use one of: alpha, arm, arm64, armel, armhf, hppa, i386, ia64, mips, mips64, mips64el, mipsel, mipsn32, mipsn32el, powerpc, ppc64, ppc64le, riscv64, s390, s390x, sh4, sparc, sparc64, v850, x32, x86_64, or none.

--os os
    Set analysis operating system, which defaults to the host operating system. Use one of: freebsd, linux, macos, netbsd, openbsd, solaris, hurd, or windows.

--i386-linux, --i386-win32, --i386-macos, --ppc-macos, --win32, --winx64
    Set analysis architecture and operating system.

--LP64, --ILP64, --LLP64, --ILP32, --LP32
    Set width of int, long and pointers, but don't override default architecture and operating system.

--16, --32, --64
    Equivalent to --LP32, --ILP32, --LP64 (on Windows: --LLP64).

--little-endian
    allow little-endian word-byte conversions

--big-endian
    allow big-endian word-byte conversions

--gcc
    use GCC as preprocessor

  Program representations:

--show-parse-tree
    show parse tree

--show-symbol-table
    show loaded symbol table

--show-goto-functions
    show loaded goto program

--list-goto-functions
    list loaded goto functions

--validate-goto-model
    enable additional well-formedness checks on the goto program

--validate-ssa-equation
    enable additional well-formedness checks on the SSA representation

  Program instrumentation options:

--bounds-check
    enable array bounds checks

--pointer-check
    enable pointer checks

--memory-leak-check
    enable memory leak checks

--memory-cleanup-check
    Enable memory cleanup checks: assert that all dynamically allocated memory is explicitly freed before terminating the program.

--div-by-zero-check
    enable division by zero checks

--signed-overflow-check
    enable signed arithmetic over- and underflow checks

--unsigned-overflow-check
    enable arithmetic over- and underflow checks

--pointer-overflow-check
    enable pointer arithmetic over- and underflow checks

--conversion-check
    check whether values can be represented after type cast

--undefined-shift-check
    check shift greater than bit-width

--float-overflow-check
    check floating-point for +/-Inf

--nan-check
    check floating-point for NaN

--enum-range-check
    checks that all enum type expressions have values in the enum range

--pointer-primitive-check
    checks that all pointers in pointer primitives are valid or null

--retain-trivial-checks
    include checks that are trivially true

--error-label label
    check that label is unreachable

--no-built-in-assertions
    ignore assertions in built-in library

--no-assertions
    ignore user assertions

--no-assumptions
    ignore user assumptions

--assert-to-assume
    convert user assertions to assumptions

--cover CC
    create test-suite with coverage criterion CC, where CC is one of assertion[s], assume[s], branch[es], condition[s], cover, decision[s], location[s], or mcdc

--cover-failed-assertions
    do not stop coverage checking at failed assertions (this is the default for --cover assertions)

--show-test-suite
    print test suite for coverage criterion (requires --cover)

--mm MM
    memory consistency model for concurrent programs (default: sc)

--malloc-may-fail
    allow malloc calls to return a null pointer

--malloc-fail-assert
    set malloc failure mode to assert-then-assume

--malloc-fail-null
    set malloc failure mode to return null

--string-abstraction
    track C string lengths and zero-termination

--dfcc-debug-lib
    enable debug assertions in the cprover contracts library

--dfcc-simple-invalid-pointer-model
    use simplified invalid pointer model in the cprover contracts library (faster, unsound)

--reachability-slice
    remove instructions that cannot appear on a trace from entry point to a property

--reachability-slice-fb
    remove instructions that cannot appear on a trace from entry point through a property

--full-slice
    run full slicer (experimental)

--drop-unused-functions
    drop functions trivially unreachable from main function

  Semantic transformations:

--nondet-static
    add nondeterministic initialization of variables with static lifetime

  BMC options:

--paths [strategy]
    explore paths one at a time

--show-symex-strategies
    list strategies for use with --paths

--show-goto-symex-steps
    show which steps symex travels, includes diagnostic information

--show-points-to-sets
    show points-to sets for pointer dereference. Requires --json-ui.

--program-only
    only show program expression

--show-byte-ops
    show all byte extracts and updates

--depth nr
    limit search depth

--max-field-sensitivity-array-size M
    maximum size M of arrays for which field sensitivity will be applied to array, the default is 64

--no-array-field-sensitivity
    deactivate field sensitivity for arrays, this is equivalent to setting the maximum field sensitivity size for arrays to 0

--show-loops
    show the loops in the program

--unwind nr
    unwind all loops at most nr times

--unwindset [T:]L:B,...
    unwind loop L with a bound of B, optionally restricted to thread T, and overriding what may be set as default unwinding via --unwind (use --show-loops to get the loop IDs)

--incremental-loop L
    check properties after each unwinding of loop L (use --show-loops to get the loop IDs)

--unwind-min nr
    start incremental-loop after nr unwindings but before solving that iteration. If for example it is 1, then the loop will be unwound once, and immediately checked. Note: this means for min-unwind 1 or 0 all properties are checked.

--unwind-max nr
    stop incremental-loop after nr unwindings

--ignore-properties-before-unwind-min
    do not check properties before unwind-min when using incremental-loop

--show-vcc
    show the verification conditions

--slice-formula
    remove assignments unrelated to property

--unwinding-assertions
    generate unwinding assertions (which are enabled by default; overrides --no-unwinding-assertions when both of these are given); cannot be used with --cover

--partial-loops
    permit paths that execute loops only partially (up to the given unwinding bound) and then continue beyond the loop even when the loop condition would still hold (such paths may be spurious, resulting in false alarms)

--no-self-loops-to-assumptions
    do not simplify while(1){} to assume(0)

--symex-complexity-limit N
    how complex (N) a path can become before symex abandons it. Currently uses guard size to calculate complexity.

--symex-complexity-failed-child-loops-limit N
    how many child branches (N) in an iteration are allowed to fail due to complexity violations before the loop gets blacklisted

--graphml-witness filename
    write the witness in GraphML format to filename

--symex-cache-dereferences
    enable caching of repeated dereferences

  Backend options:

--object-bits n
    number of bits used for object addresses

--sat-solver solver
    use specified SAT solver

--external-sat-solver cmd
    command to invoke SAT solver process

--no-sat-preprocessor
    disable the SAT solver's simplifier

--dimacs
    generate CNF in DIMACS format

--beautify
    beautify the counterexample (greedy heuristic)

--smt1
    use default SMT1 solver (obsolete)

--smt2
    use default SMT2 solver (Z3)

--bitwuzla
    use Bitwuzla

--boolector
    use Boolector

--cprover-smt2
    use CPROVER SMT2 solver

--cvc3
    use CVC3

--cvc4
    use CVC4

--cvc5
    use CVC5

--mathsat
    use MathSAT

--yices
    use Yices

--z3
    use Z3

--fpa
    use theory of floating-point arithmetic

--refine
    use refinement procedure (experimental)

--refine-arrays
    use refinement for arrays only

--refine-arithmetic
    refinement of arithmetic expressions only

--max-node-refinement
    maximum refinement iterations for arithmetic expressions

--incremental-smt2-solver cmd
    Use the incremental SMT backend where cmd is the command to invoke the SMT solver of choice.
    Example invocations:
      --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
      --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' (use the CVC5 solver).

    Note that:
    The solver name must be in the "PATH" or be an executable with full path.
    The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
    The SMT solver should support the QF_AUFBV logic.

--outfile filename
    output formula to given file

--dump-smt-formula filename
    output smt incremental formula to the given file

--write-solver-stats-to json-file
    collect the solver query complexity

--refine-strings
    use string refinement (experimental)

--string-printable
    restrict to printable strings (experimental)

--arrays-uf-never
    never turn arrays into uninterpreted functions

--arrays-uf-always
    always turn arrays into uninterpreted functions

--show-array-constraints
    show array theory constraints added during post processing. Requires --json-ui.

  User-interface options:

--xml-ui
    use XML-formatted output

--xml-interface
    bi-directional XML interface

--json-ui
    use JSON-formatted output

--json-interface
    bi-directional JSON interface

--trace-json-extended
    add rawLhs property to trace

--trace-show-function-calls
    show function calls in plain trace

--trace-show-code
    show original code in plain trace

--trace-hex
    represent plain trace values in hex

--compact-trace
    give a compact trace

--stack-trace
    give a stack trace only

--flush
    flush every line of output

--export-symex-ready-goto filename
    export the symex ready version of the goto-model into the given filename

--verbosity #
    verbosity level

--timestamp [monotonic|wall]
    Print microsecond-precision timestamps. monotonic: stamps increase monotonically. wall: ISO-8601 wall clock timestamps.

ENVIRONMENT
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.

BUGS
If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues

SEE ALSO
goto-cc(1), goto-instrument(1)

COPYRIGHT
2001-2016, Daniel Kroening, Edmund Clarke