Command line options are split into several categories. Each table below describes options of one category.
You can obtain a similar information directly from JBMC tool by running it with the option --help.
Program instrumentation options
| Option | Description |
|---|
| --bounds-check | enable array bounds checks |
| --pointer-check | enable pointer checks (always enabled for Java) |
| --memory-leak-check | enable memory leak checks |
| --div-by-zero-check | enable division by zero checks |
| --signed-overflow-check | enable signed arithmetic over- and underflow checks |
| --unsigned-overflow-check | enable arithmetic over- and underflow checks |
| --pointer-overflow-check | enable pointer arithmetic over- and underflow checks |
| --conversion-check | check whether values can be represented after type cast |
| --undefined-shift-check | check shift greater than bit-width |
| --float-overflow-check | check floating-point for +/-Inf |
| --nan-check | check floating-point for NaN |
| --no-built-in-assertions | ignore assertions in built-in library |
| --no-assertions | ignore user assertions |
| --no-assumptions | ignore user assumptions |
| --error-label label | check that label is unreachable |
| --cover CC | create test-suite with coverage criterion CC |
| --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
| Option | Description |
|---|
| --classpath dir/jar | set the classpath to load additional jar files or class files |
| --main-class class-name | set the name of the main class |
| --no-core-models | don't load internally provided models for core classes in the Java Class Library |
| --java-assume-inputs-non-null | never initialize reference-typed parameter to the entry point with null |
| --java-throw-runtime-exceptions | make implicit runtime exceptions explicit (propagate them instead of checking whether they occur) |
| --java-max-input-array-length N | limit input array size to <= N |
| --java-max-input-tree-depth N | object references are (deterministically) set to null in the object |
| --java-max-vla-length | limit the length of user-code-created arrays |
| --java-cp-include-files | regexp or JSON list of files to load (with '@' prefix) |
| --lazy-methods | only translate methods that appear to be reachable from the --function entry point or main class Note --show-symbol-table/goto-functions/properties output will be restricted to loaded methods in this case |
| --lazy-methods-extra-entry-point METHODNAME | treat METHODNAME as a possible program entry point for the purpose of lazy method loading A '.*' wildcard is allowed to specify all class members |
| --java-unwind-enum-static | try to unwind loops in static initialization of enums |
| --symex-driven-lazy-loading | only load functions when first entered by symbolic execution Note --show-symbol-table/goto-functions/properties output will be restricted to loaded methods in this case, and only output after the symex phase |
BMC options
| Option | Description |
|---|
| --paths | explore paths one at a time |
| --program-only | only show program expression |
| --show-loops | show the loops in the program |
| --depth nr | limit search depth |
| --unwind nr | unwind nr times |
| --unwindset L:B,... | unwind loop L with a bound of B (use --show-loops to get the loop IDs) |
| --show-vcc | show the verification conditions |
| --slice-formula | remove assignments unrelated to property |
| --unwinding-assertions | generate unwinding assertions |
| --partial-loops | permit paths with partial loops |
| --no-pretty-names | do not simplify identifiers |
| --graphml-witness filename | write the witness in GraphML format to filename |
Backend options
| Option | Description |
|---|
| --object-bits n | number of bits used for object addresses |
| --dimacs | generate CNF in DIMACS format |
| --beautify | beautify the counterexample (greedy heuristic) |
| --localize-faults | localize faults (experimental) |
| --smt1 | use default SMT1 solver (obsolete) |
| --smt2 | use default SMT2 solver (Z3) |
| --boolector | use Boolector |
| --mathsat | use MathSAT |
| --cvc4 | use CVC4 |
| --yices | use Yices |
| --z3 | use Z3 |
| --refine | use refinement procedure (experimental) |
| --refine-strings | use string refinement (experimental) |
| --string-printable | add constraint that strings are printable (experimental) |
| --string-max-length | add constraint on the length of strings for the string solver |
| --string-max-input-length | add constraint on the length of input strings |
| --max-nondet-string-length n | bounds the maximum length n of non-deterministic strings (default: unrestricted) |
| --outfile filename | output formula to given file |
| --arrays-uf-never | never turn arrays into uninterpreted functions |
| --arrays-uf-always | always turn arrays into uninterpreted functions |