jbmc(1)

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.