Provided by: cbmc_5.10-5ubuntu1_amd64 bug

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

OPTIONS

   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)

       --smt2 Output subgoals in SMT2 syntax

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

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. GOTO-CC aims to accept all  environment  variables  that
       GCC does.

COPYRIGHT

       2001-2016, Daniel Kroening, Edmund Clarke