Provided by: cbmc_5.3-1_amd64 bug


       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


   FRONTEND OPTIONS (cbmc and goto-cc)
       -I path
              Set include path (C/C++)

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

              Stop after preprocessing

              Show symbol table

              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

       --16, --32, --64
              Set width of int

       --LP64, --ILP64, --LLP64, --ILP32, --LP32
              Set width of int, long and pointers

              Allow little-endian word-byte conversions

              Allow big-endian word-byte conversions

              Make "char" unsigned by default

       --arch Set target architecture

       --os   Set target operating system

              Don't set up an architecture

              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

   PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)
       Both cbmc and goto-instrument can generate assertions that catch specific  common  errors,
       as listed below.

              Enable array bounds checks

              Enable division by zero checks

              Enable pointer checks

              Enable arithmetic over- and underflow checks for signed integer arithmetic

              Enable arithmetic over- and underflow checks for unsigned integer arithmetic

              Check floating-point computations for NaN

              Ignore user-provided assertions

              Ignore user-provided assumptions

       --error-label label
              Check that the given label is unreachable

       goto-instrument supports further, more complex, program transformations.

              Makes reads from volatile variables non-deterministic

       --isr function
              Instruments an interrupt service routine with the given name

       --mmio Instruments memory-mapped I/O

              Variables with static lifetime are initialized non-deterministically

              Output ANSI-C source code instead of a goto binary.

   BMC OPTIONS (cbmc)
              Report status of all properties

              Only show properties

              Show the loops in the program

              Check which assertions are reachable

       --function name
              Set main function name

       --property id
              Only check specific property with given identifier

              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 the verification conditions

              Remove assignments unrelated to property

              Do not generate unwinding assertions

              Do not simplify identifiers

              Generate CNF in DIMACS format for use by external SAT solvers

              Beautify the counterexample (greedy heuristic)

       --smt1 Output subgoals in SMT1 syntax (experimental)

       --smt2 Output subgoals in SMT2 syntax (experimental)

              Use Boolector (experimental)

              Use MathSAT (experimental)

       --cvc  Use CVC3 (experimental)

              Use Yices (experimental)

       --z3   Use Z3 (experimental)

              Use refinement procedure (experimental)

       --outfile filename
              Output formula to given file

              Never turn arrays into uninterpreted functions

              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