Scroll to navigation

JBMC(1) User Commands JBMC(1)

NAME

jbmc - Bounded model checking for Java bytecode

SYNOPSIS

show help
Use the fully qualified name of a method as entry point, e.g., 'mypackage.Myclass.foo:(I)Z'
The entry point is the method specified by --function, or otherwise, the public static void main(String[]) method of the given class class-name.
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).
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

Set class search path of directories and jar files using a colon-separated list of directories and JAR archives to search for class files.
Set the name of the main class.
Set entry point function name.

Analysis options:

show the properties, but don't run analysis
generate a Cobertura XML coverage report in f
only check one specific property
give a counterexample trace for failed properties
stop analysis once a failed property is detected (implies --trace)
localize faults (experimental)
throw an error if the structure of the counterexample trace does not match certain assumptions (experimental, currently java only)

Platform options:

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.
Set analysis operating system, which defaults to the host operating system. Use one of: freebsd, linux, macos, solaris, or windows.
Set analysis architecture and operating system.
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).
allow little-endian word-byte conversions
allow big-endian word-byte conversions
use GCC as preprocessor

Program representations:

show parse tree
show loaded symbol table
list symbols with type information
show loaded goto program
list loaded goto functions
drop functions trivially unreachable from main function
show the class hierarchy

Program instrumentation options:

ignore user assertions
ignore user assumptions
memory consistency model for concurrent programs
remove instructions that cannot appear on a trace from entry point to a property
remove instructions that cannot appear on a trace from entry point through a property
run full slicer (experimental)

Java Bytecode frontend options:

ignore uncaught exceptions and errors
Throw java.lang.AssertionError on violated assert statements instead of failing at the location of the assert statement.
Make implicit runtime exceptions explicit.
Transform throw instructions into assert FALSE followed by assume FALSE.
Limit nondet (e.g. input) array size to at most N.
Limit size of nondet (e.g. input) object tree; at level N references are set to null.
Never initialize reference-typed parameter to the entry point with null.
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.
Force float and double inputs to have integer values; does not work for arrays;
Limit the length of user-code-created arrays to N.
Regular expression or JSON list of files to load (with '@' prefix).
Also load code from class CLASS.
Never load code from class 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.
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'.
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.
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.
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.
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.
enable java multi-threading support (experimental)
unwind loops in static initialization of enums
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:

add nondeterministic initialization of variables with static lifetime

BMC options:

explore paths one at a time
list strategies for use with --paths
show which steps symex travels, includes diagnostic information
show points-to sets for pointer dereference. Requires --json-ui.
only show program expression
show all byte extracts and updates
limit search depth
maximum size M of arrays for which field sensitivity will be applied to array, the default is 64
deactivate field sensitivity for arrays, this is equivalent to setting the maximum field sensitivity size for arrays to 0
show the loops in the program
unwind nr times
unwind loop L with a bound of B (optionally restricted to thread T) (use --show-loops to get the loop IDs)
check properties after each unwinding of loop L (use --show-loops to get the loop IDs)
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.
stop incremental-loop after nr unwindings
do not check properties before unwind-min when using incremental-loop
show the verification conditions
remove assignments unrelated to property
generate unwinding assertions (cannot be used with --cover)
permit paths with partial loops
do not simplify while(1){} to assume(0)
how complex (N) a path can become before symex abandons it. Currently uses guard size to calculate complexity.
how many child branches (N) in an iteration are allowed to fail due to complexity violations before the loop gets blacklisted
write the witness in GraphML format to filename
enable caching of repeated dereferences

Backend options:

number of bits used for object addresses
use specified SAT solver
command to invoke SAT solver process
disable the SAT solver's simplifier
generate CNF in DIMACS format
beautify the counterexample (greedy heuristic)
use default SMT1 solver (obsolete)
use default SMT2 solver (Z3)
use Boolector
use Boolector
use CPROVER SMT2 solver
use CVC3
use CVC4
use CVC5
use MathSAT
use Yices
use Z3
use theory of floating-point arithmetic
use refinement procedure (experimental)
use refinement for arrays only
refinement of arithmetic expressions only
maximum refinement iterations for arithmetic expressions
command to invoke external SMT solver for incremental solving (experimental)
output formula to given file
output smt incremental formula to the given file
collect the solver query complexity
turn off string refinement
restrict to printable strings and characters
restrict to non-empty strings (experimental)
restrict non-null strings to a fixed value st; the switch can be used multiple times to give several strings
Default is 67108863; note that setting the value higher than this does not work with --trace or --validate-trace.
never turn arrays into uninterpreted functions
always turn arrays into uninterpreted functions

Other options:

show version and exit
use XML-formatted output
bi-directional XML interface
use JSON-formatted output
bi-directional JSON interface
enable additional well-formedness checks on the goto program
enable additional well-formedness checks on the SSA representation
add rawLhs property to trace
show function calls in plain trace
show original code in plain trace
represent plain trace values in hex
give a compact trace
give a stack trace only
flush every line of output
verbosity level
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

June 2022 jbmc-5.59.0