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

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

cbmc-5.59.0                                         June 2022                                            CBMC(1)