NAME

       jbmc - Bounded model checking for Java bytecode

SYNOPSIS

       jbmc [-?] [-h] [--help]
              show help

       jbmc method-name
              Use the fully qualified name of a method as entry point, e.g., 'mypackage.Myclass.foo:(I)Z'

       jbmc class-name
              The  entry  point  is  the  method  specified  by --function, or otherwise, the public static void
              main(String[]) method of the given class class-name.

       jbmc -jar jarfile
              JAR file to be checked.  The entry point is the method specified by --function or  otherwise,  the
              public  static void main(String[]) method of the class specified by --main-class or the main class
              specified in the JAR manifest (checked in this order).

       jbmc --gb goto-binary
              GOTO binary file to be checked.  The entry  point  is  the  method  specified  by  --function,  or
              otherwise,  the  public static void main(String[]) of the class specified by --main-class (checked
              in this order).

DESCRIPTION

OPTIONS

       -classpath dirs/jars, -cp dirs/jars, --classpath dirs/jars
              Set class search path of directories and jar files using a colon-separated list of directories and
              JAR archives to search for class files.

       --main-class class-name
              Set the name of the main class.

       --function name
              Set entry point function name.

   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)

       --validate-trace
              throw an error if the structure of the counterexample trace does  not  match  certain  assumptions
              (experimental, currently java only)

   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

       --list-symbols
              list symbols with type information

       --show-goto-functions
              show loaded goto program

       --list-goto-functions
              list loaded goto functions

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

       --show-class-hierarchy
              show the class hierarchy

   Program instrumentation options:
       --no-assertions
              ignore user assertions

       --no-assumptions
              ignore user assumptions

       --mm MM
              memory consistency model for concurrent programs

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

   Java Bytecode frontend options:
       --disable-uncaught-exception-check
              ignore uncaught exceptions and errors

       --throw-assertion-error
              Throw java.lang.AssertionError on violated assert statements instead of failing at the location of
              the assert statement.

       --throw-runtime-exceptions
              Make implicit runtime exceptions explicit.

       --assert-no-exceptions-thrown
              Transform throw instructions into assert FALSE followed by assume FALSE.

       --max-nondet-array-length N
              Limit nondet (e.g. input) array size to at most N.

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

       --java-assume-inputs-non-null
              Never initialize reference-typed parameter to the entry point with null.

       --java-assume-inputs-interval [L:U] or [L:] or [:U]
              Force  numerical  primitive-typed inputs (byte, short, int, long, float, double) to be initialized
              within the given range; lower bound L and upper bound U  must  be  integers;  does  not  work  for
              arrays.

       --java-assume-inputs-integral
              Force float and double inputs to have integer values; does not work for arrays;

       --java-max-vla-length N
              Limit the length of user-code-created arrays to N.

       --java-cp-include-files r
              Regular expression or JSON list of files to load (with '@' prefix).

       --java-load-class CLASS
              Also load code from class CLASS.

       --java-no-load-class CLASS
              Never load code from class CLASS.

       --ignore-manifest-main-class
              Ignore  Main-Class  entries  in  JAR  manifest files.  If this option is specified and the options
              --function and --main-class are not, we can be certain that  all  classes  in  the  JAR  file  are
              loaded.

       --context-include i, --context-exclude e
              Only   analyze   code   matching   specification  i  that  does  not  match  specification  e,  if
              --context-exclude e is also used.  All other methods are excluded, i.e., we load their  signatures
              and  meta-information, but not their bodies.  A specification is any prefix of a package, class or
              method       name,       e.g.       "org.cprover."       or       "org.cprover.MyClass."        or
              "org.cprover.MyClass.methodToStub:(I)Z".   These options can be given multiple times.  The default
              for context-include is 'all included'; default for context-exclude is 'nothing excluded'.

       --no-lazy-methods
              Load and translate all methods given on the command line and in --classpath  Default  is  to  load
              methods  that  appear  to  be  reachable from the --function entry point or main class.  Note that
              --show-symbol-table, --show-goto-functions and --show-properties output are restricted  to  loaded
              methods by default.

       --lazy-methods-extra-entry-point METHODNAME
              Treat  METHODNAME  as  a  possible  program  entry  point  for the purpose of lazy method loading.
              METHODNAME can be a regular expression that will be matched against all  symbols.  If  missing,  a
              java::  prefix  will  be  added. If no descriptor is found, all overloads of a method will also be
              added.

       --static-values f
              Load initial values of static fields from the given JSON file. We assign static  fields  to  these
              values  instead  of  calling the normal static initializer (clinit) method.  The argument can be a
              relative or absolute path to the file.

       --java-lift-clinit-calls
              Lifts clinit calls in function bodies to the top of the function. This may reduce the overall cost
              of static initialisation, but may be unsound if  there  are  cyclic  dependencies  between  static
              initializers  due to potentially changing their order of execution, or if static initializers have
              side-effects such as updating another class' static field.

       --java-threading
              enable java multi-threading support (experimental)

       --java-unwind-enum-static
              unwind loops in static initialization of enums

       --symex-driven-lazy-loading
              only load functions when first entered  by  symbolic  execution.  Note  that  --show-symbol-table,
              --show-goto-functions/properties  output  will  be  restricted to loaded methods in this case, and
              only output after the symex phase.

   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

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

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

       --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
              command to invoke external SMT solver for incremental solving (experimental)

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

       --no-refine-strings
              turn off string refinement

       --string-printable
              restrict to printable strings and characters

       --string-non-empty
              restrict to non-empty strings (experimental)

       --string-input-value st
              restrict non-null strings to a fixed value st; the switch can  be  used  multiple  times  to  give
              several strings

       --max-nondet-string-length n bound the length of nondet (e.g. input) strings.
              Default  is  67108863;  note that setting the value higher than this does not work with --trace or
              --validate-trace.

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

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

   Other options:
       --version
              show version and exit

       --xml-ui
              use XML-formatted output

       --xml-interface
              bi-directional XML interface

       --json-ui
              use JSON-formatted output

       --json-interface
              bi-directional JSON interface

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

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

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

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

BUGS

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

SEE ALSO

       cbmc(1), janalyzer(1), jdiff(1)

COPYRIGHT

       2001-2018, Daniel Kroening, Edmund Clarke

jbmc-5.59.0                                         June 2022                                            JBMC(1)