JBMC(1)

📦
version 6.6.0 · 2 versions
  • 6.6.0 · debian trixie, ubuntu questing, ubuntu resolute, ubuntu stonking (latest)
  • 5.12 · ubuntu jammy
, in debian trixie, ubuntu questing, ubuntu resolute, ubuntu stonking

💅 JBMC(1) — User Commands 🎀

okay so bestie, welcome to the jbmc manual page — it's filed under User Commands in the manuals, and it's literally the whole guide to Bounded model checking for Java bytecode. Buckle up, it's long, and we're doing every single flag. no skipping. periodt. 💖

✨ NAME ✨

jbmc — Bounded model checking for Java bytecode 🦋

✨ SYNOPSIS ✨

here's the whole shape of it, untouched, exactly as written:

jbmc [-?] [-h] [--help]
       show help

jbmc method-name
       Use the fully qualified name of a method as entry point, e.g.,
       'mypackage.Myclass.foo:(I)Z'

jbmc class-name
       The entry point is the method specified by --function, or
       otherwise, the public static void main(String[]) method of the
       given class class-name.

jbmc -jar jarfile
       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).

jbmc --gb goto-binary
       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).

so let's vibe-check each one, one at a time 💅

  • jbmc [-?] [-h] [--help] — the "help me bestie" invocation. It shows the help. that's it, that's the whole job 🫶
  • jbmc method-name — hand it the fully qualified name of a method and that method becomes your entry point. like, for real fully qualified, e.g. 'mypackage.Myclass.foo:(I)Z' 👑
  • jbmc class-name — give it a class name instead. the entry point is whatever method --function says, or if you didn't set that, it's the public static void main(String[]) method of the class class-name.
  • jbmc -jar jarfile — checking a whole JAR file. entry point order is: the method from --function, otherwise the public static void main(String[]) of the class from --main-class, otherwise the main class in the JAR manifest. and yes, it checks them in this order, no cap.
  • jbmc --gb goto-binary — feeding it a GOTO binary file. entry point is the method from --function, otherwise the public static void main(String[]) of the class from --main-class. again: checked in this order ✨

✨ DESCRIPTION ✨

okay so the original page has this heading and then… nothing. it's giving minimalism. iconic of it honestly 💀. the whole description lives in the options below, so let's go.

✨ OPTIONS ✨

🌸 the basics, aka how do i even point this thing at my code

  • -classpath dirs/jars, -cp dirs/jars, --classpath dirs/jars — set the class search path for directories and jar files. you give it a colon-separated list of directories and JAR archives and it goes hunting for class files in there 🧚
  • --main-class class-name — sets the name of the main class.
  • --function name — sets the entry point function name.

🔍 Analysis options:

  • --show-properties — show the properties, but do not run the analysis. just a little peek, no commitment 👀
  • --symex-coverage-report f — generate a Cobertura XML coverage report, written into f.
  • --property id — only check one specific property. just the one. main character property 💅
  • --trace — give a counterexample trace for failed properties. receipts for the fail 📜
  • --stop-on-fail — stop the analysis the second a failed property shows up. this implies --trace, so you get the receipts too.
  • --localize-faults — localize faults. it's experimental, bestie.
  • --validate-trace — throws an error if the structure of the counterexample trace doesn't match certain assumptions. also experimental, and currently java only.

🌈 Platform options:

  • --arch arch — set the analysis architecture. 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 the analysis operating system. 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 the analysis architecture and operating system, in one lil combo move.
  • --LP64, --ILP64, --LLP64, --ILP32, --LP32 — set the width of int, long and pointers. note that this does not override the default architecture and operating system 🫶
  • --16, --32, --64 — equivalent to --LP32, --ILP32, --LP64 respectively (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 the parse tree 🌳
  • --show-symbol-table — show the loaded symbol table.
  • --list-symbols — list symbols, with type information.
  • --show-goto-functions — show the loaded goto program.
  • --list-goto-functions — list the loaded goto functions.
  • --drop-unused-functions — drop functions that are trivially unreachable from the main function. bye, you're not needed 💀
  • --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 the entry point to a property.
  • --reachability-slice-fb — remove instructions that cannot appear on a trace from the entry point through a property.
  • --full-slice — run the full slicer. it's 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 the size of the nondet (e.g. input) object tree; at level N, references are set to null.
  • --java-assume-inputs-non-null — never initialize a 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. the lower bound L and upper bound U must be integers. heads up: this 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 a '@' 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, then we can be certain that all classes in the JAR file are loaded. cute little guarantee 💖
  • --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, because it can potentially change 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 the 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: the solver menu ✨

  • --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: the little extras 🎀

  • --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.

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)

2001-2018, Daniel Kroening, Edmund Clarke

Okay bestie, that's the whole page. This is JBMC(1), from jbmc-5.59.0, dated June 2022. Go verify something cute. 💅✨

📦 where this page comes from