jbmc(1) on Linux
The text 8c872a4156a1, as Debian 13 (Trixie) shipped it. The page shows this text now.
Bounded model checking for Java bytecode
Flags it lists
-
--16 -
--32 -
--64 -
--ILP32 -
--ILP64 -
--LLP64 -
--LP32 -
--LP64 -
--arch -
--arrays-uf-always -
--arrays-uf-never -
--assert-no-exceptions-thrown -
--beautify -
--big-endian -
--bitwuzla -
--boolector -
--classpath -
--compact-trace -
--context-exclude -
--context-include -
--cprover-smt2 -
--cvc3 -
--cvc4 -
--cvc5 -
--depth -
--dimacs -
--disable-uncaught-exception-check -
--drop-unused-functions -
--dump-smt-formula -
--external-sat-solver -
--flush -
--fpa -
--full-slice -
--function -
--gcc -
--graphml-witness -
--i386-linux -
--i386-macos -
--i386-win32 -
--ignore-manifest-main-class -
--ignore-properties-before-unwind-min -
--incremental-loop -
--incremental-smt2-solver -
--java-assume-inputs-integral -
--java-assume-inputs-non-null -
--java-cp-include-files -
--java-lift-clinit-calls -
--java-load-class -
--java-max-vla-length -
--java-no-load-class -
--java-threading -
--java-unwind-enum-static -
--json-interface -
--json-ui -
--lazy-methods-extra-entry-point -
--list-goto-functions -
--list-symbols -
--little-endian -
--localize-faults -
--main-class -
--mathsat -
--max-field-sensitivity-array-size -
--max-node-refinement -
--max-nondet-array-length -
--max-nondet-tree-depth -
--mm -
--no-array-field-sensitivity -
--no-assertions -
--no-assumptions -
--no-lazy-methods -
--no-refine-strings -
--no-sat-preprocessor -
--no-self-loops-to-assumptions -
--no-unwinding-assertions -
--nondet-static -
--object-bits -
--os -
--outfile -
--partial-loops -
--paths -
--ppc-macos -
--program-only -
--property -
--reachability-slice -
--reachability-slice-fb -
--refine -
--refine-arithmetic -
--refine-arrays -
--sat-solver -
--show-byte-ops -
--show-class-hierarchy -
--show-goto-functions -
--show-goto-symex-steps -
--show-loops -
--show-parse-tree -
--show-points-to-sets -
--show-properties -
--show-symbol-table -
--show-symex-strategies -
--show-vcc -
--slice-formula -
--smt1 -
--smt2 -
--stack-trace -
--static-values -
--stop-on-fail -
--string-input-value -
--string-non-empty -
--string-printable -
--symex-cache-dereferences -
--symex-complexity-failed-child-loops-limit -
--symex-complexity-limit -
--symex-coverage-report -
--symex-driven-lazy-loading -
--throw-assertion-error -
--throw-runtime-exceptions -
--timestamp -
--trace -
--trace-hex -
--trace-json-extended -
--trace-show-code -
--trace-show-function-calls -
--unwind -
--unwind-max -
--unwind-min -
--unwinding-assertions -
--unwindset -
--validate-goto-model -
--validate-ssa-equation -
--validate-trace -
--verbosity -
--version -
--win32 -
--winx64 -
--write-solver-stats-to -
--xml-interface -
--xml-ui -
--yices -
--z3 -
-classpath -
-cp