JBMC(1)

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