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

       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

   Analysis options:
       --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, solaris, 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

       --havoc-undefined-functions
              for  any  function  that  has no body, assign non-deterministic values to any parameters passed as
              non-const pointers and the return value

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

       --unwindset [T:]L:B,...
              unwind  loop  L with a bound of B (optionally restricted to thread T) (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 (cannot be used with --cover)

       --partial-loops
              permit paths with partial loops

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