Provided by: jbmc_5.95.1-4ubuntu1_amd64 
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, 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
--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 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 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)