Command line options of JBMC

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.

Analysis options
--show-propertiesshow the properties, but don't run analysis
--symex-coverage-report fgenerate a Cobertura XML coverage report in f
--property idonly check one specific property
--stop-on-failstop analysis once a failed property is detected
--tracegive a counterexample trace for failed properties
--function nameset the function name as a custom entry point the the program (instead of the standard main function)

Program representations
--show-parse-treeshow parse tree
--show-symbol-tableshow loaded symbol table
--show-goto-functionsshow loaded goto program
--list-goto-functionslist loaded goto functions
--drop-unused-functionsdrop functions trivially unreachable from main function

Program instrumentation options
--bounds-checkenable array bounds checks
--pointer-checkenable pointer checks (always enabled for Java)
--memory-leak-checkenable memory leak checks
--div-by-zero-checkenable division by zero checks
--signed-overflow-checkenable signed arithmetic over- and underflow checks
--unsigned-overflow-checkenable arithmetic over- and underflow checks
--pointer-overflow-checkenable pointer arithmetic over- and underflow checks
--conversion-checkcheck whether values can be represented after type cast
--undefined-shift-checkcheck shift greater than bit-width
--float-overflow-checkcheck floating-point for +/-Inf
--nan-checkcheck floating-point for NaN
--no-built-in-assertionsignore assertions in built-in library
--no-assertionsignore user assertions
--no-assumptionsignore user assumptions
--error-label labelcheck that label is unreachable
--cover CCcreate test-suite with coverage criterion CC
--mm MMmemory consistency model for concurrent programs
--reachability-sliceremove instructions that cannot appear on a trace from entry point to a property
--reachability-slice-fbremove instructions that cannot appear on a trace from entry point through a property
--full-slicerun full slicer (experimental)

Java Bytecode frontend options
--classpath dir/jarset the classpath to load additional jar files or class files
--main-class class-nameset the name of the main class
--no-core-modelsdon't load internally provided models for core classes in the Java Class Library
--java-assume-inputs-non-nullnever initialize reference-typed parameter to the entry point with null
--java-throw-runtime-exceptionsmake implicit runtime exceptions explicit (propagate them instead of checking whether they occur)
--java-max-input-array-length Nlimit input array size to <= N
--java-max-input-tree-depth Nobject references are (deterministically) set to null in the object
--java-max-vla-lengthlimit the length of user-code-created arrays
--java-cp-include-filesregexp or JSON list of files to load (with '@' prefix)
--lazy-methodsonly 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 METHODNAMEtreat 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-statictry to unwind loops in static initialization of enums
--symex-driven-lazy-loadingonly 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
--pathsexplore paths one at a time
--program-onlyonly show program expression
--show-loopsshow the loops in the program
--depth nrlimit search depth
--unwind nrunwind nr times
--unwindset L:B,...unwind loop L with a bound of B (use --show-loops to get the loop IDs)
--show-vccshow the verification conditions
--slice-formularemove assignments unrelated to property
--unwinding-assertionsgenerate unwinding assertions
--partial-loopspermit paths with partial loops
--no-pretty-namesdo not simplify identifiers
--graphml-witness filenamewrite the witness in GraphML format to filename

Backend options
--object-bits nnumber of bits used for object addresses
--dimacsgenerate CNF in DIMACS format
--beautifybeautify the counterexample (greedy heuristic)
--localize-faultslocalize faults (experimental)
--smt1use default SMT1 solver (obsolete)
--smt2use default SMT2 solver (Z3)
--boolectoruse Boolector
--mathsatuse MathSAT
--cvc4use CVC4
--yicesuse Yices
--z3use Z3
--refineuse refinement procedure (experimental)
--refine-stringsuse string refinement (experimental)
--string-printableadd constraint that strings are printable (experimental)
--string-max-lengthadd constraint on the length of strings for the string solver
--string-max-input-lengthadd constraint on the length of input strings
--max-nondet-string-length nbounds the maximum length n of non-deterministic strings (default: unrestricted)
--outfile filenameoutput formula to given file
--arrays-uf-nevernever turn arrays into uninterpreted functions
--arrays-uf-alwaysalways turn arrays into uninterpreted functions

Other options
--versionshow version and exit
--xml-uiuse XML-formatted output
--json-uiuse JSON-formatted output
--trace-json-extendedadd rawLhs property to trace
--verbosity #verbosity level
--timestamp <monotonic|wall>print microsecond-precision timestamps. monotonic: stamps increase monotonically. wall: ISO-8601 wall clock timestamps.