Package org.bmc4j.gradle

Class BmcExtensionConfig

java.lang.Object
org.bmc4j.gradle.BmcExtensionConfig
public abstract class BmcExtensionConfig extends Object
The bmc { } DSL block. 

 bmc {
     unwind = 16                       // default loop bound for proofs
     // jbmcPath = "/opt/cbmc/bin/jbmc" // use a local binary instead of the bundled engine
 }

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static class 
    BmcExtensionConfig.ModelSpec
    The models { conformant(...) / domain(...) } DSL block.

  • Constructor Summary

    Constructors
    Constructor
    Description
    BmcExtensionConfig()
     

  • Method Summary

    Modifier and Type
    Method
    Description
    abstract org.gradle.api.provider.ListProperty<String>
    getAllowStubs()
    Build-wide acknowledged nondet stubs: methods every proof may rely on as havoc'd stand-ins without warning.
    abstract org.gradle.api.provider.Property<Boolean>
    getCache()
    Per-proof verdict caching.
    abstract org.gradle.api.provider.Property<String>
    getJbmcPath()
    Optional path to an existing JBMC binary.
    abstract BmcExtensionConfig.ModelSpec
    getModelSpec()
    Registered user models with their declared intent.
    abstract org.gradle.api.provider.Property<Integer>
    getParallelism()
    How many proofs to verify concurrently — each runs its own jbmc process, and proofs are independent, so this scales near-linearly.
    abstract org.gradle.api.provider.Property<Boolean>
    getProgress()
    Show per-proof progress while the test task runs ("proving X", "OK/REFUTED X (Ns)") plus a final summary, at Gradle's lifecycle level so it's visible in a normal gradlew test.
    abstract org.gradle.api.provider.Property<String>
    getSolver()
    SAT/SMT backend for JBMC.
    abstract org.gradle.api.provider.Property<String>
    getSolverCmd()
    Path/command for an external SMT2 solver binary (used with --smt2); overrides getSolver().
    abstract org.gradle.api.provider.Property<String>
    getSolverPath()
    Directory holding the SMT solver binary (e.g.
    abstract org.gradle.api.provider.Property<Boolean>
    getStrictModels()
    Strict user-model mode, the strictStubs analog.
    abstract org.gradle.api.provider.Property<Boolean>
    getStrictStubs()
    Strict nondet-stub mode.
    abstract org.gradle.api.provider.Property<Integer>
    getTimeoutSeconds()
    Default per-proof wall-clock budget in seconds.
    abstract org.gradle.api.provider.Property<Integer>
    getUnwind()
    Default loop/recursion unwinding bound for proofs that don't override it.
    abstract org.gradle.api.provider.ListProperty<String>
    getUserPackages()
    Package prefixes of the module under test.
    void
    models(org.gradle.api.Action<? super BmcExtensionConfig.ModelSpec> action)
    Configure the registered user models -- see getModelSpec().

    Methods inherited from class java.lang.Object

    clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Constructor Details

    • BmcExtensionConfig

      public BmcExtensionConfig()

  • Method Details

    • getJbmcPath

      public abstract org.gradle.api.provider.Property<String> getJbmcPath()
      Optional path to an existing JBMC binary. When set, the bundled engine dependency is not added and this binary is used instead — useful for an internal mirror, a custom build, or air-gapped environments.

    • getUnwind

      public abstract org.gradle.api.provider.Property<Integer> getUnwind()
      Default loop/recursion unwinding bound for proofs that don't override it.

    • getTimeoutSeconds

      public abstract org.gradle.api.provider.Property<Integer> getTimeoutSeconds()
      Default per-proof wall-clock budget in seconds. When a proof doesn't reach a verdict in time, its engine process tree is force-killed and the proof is reported UNKNOWN (undecided — still fails, but distinctly from a refutation). A proof's @BmcProof(timeoutSeconds=…) overrides this. Unset / 0 means no timeout (proofs run to completion). Overridable at the command line with -Dbmc.timeoutSeconds.

    • getParallelism

      public abstract org.gradle.api.provider.Property<Integer> getParallelism()
      How many proofs to verify concurrently — each runs its own jbmc process, and proofs are independent, so this scales near-linearly. Defaults to the number of available processors. Set to 1 to run proofs serially (e.g. if heavy proofs strain memory).

    • getSolver

      public abstract org.gradle.api.provider.Property<String> getSolver()
      SAT/SMT backend for JBMC. Default is JBMC's built-in MiniSat. SMT solvers ("z3", "boolector", "cvc4", "cvc5") — which must be on PATH — can be much faster on array/bitvector-heavy proofs; any other value is passed to --sat-solver (e.g. "cadical", "glucose").

    • getSolverCmd

      public abstract org.gradle.api.provider.Property<String> getSolverCmd()
      Path/command for an external SMT2 solver binary (used with --smt2); overrides getSolver(). Use when the solver isn't on PATH.

    • getSolverPath

      public abstract org.gradle.api.provider.Property<String> getSolverPath()
      Directory holding the SMT solver binary (e.g. the dir containing z3). It's prepended to jbmc's PATH so getSolver() / @BmcProof(solver=…) can find the solver without it being on the global PATH. Keep machine-specific paths out of the repo — set it from a Gradle property, e.g. solverPath = providers.gradleProperty("z3Path").orNull.

    • getProgress

      public abstract org.gradle.api.provider.Property<Boolean> getProgress()
      Show per-proof progress while the test task runs ("proving X", "OK/REFUTED X (Ns)") plus a final summary, at Gradle's lifecycle level so it's visible in a normal gradlew test. On by default — proofs can take seconds each, and silence looks like a hang. Set to false for quiet CI logs.

    • getCache

      public abstract org.gradle.api.provider.Property<Boolean> getCache()
      Per-proof verdict caching. When true (the default), a proof that verified and whose inputs (bytecode, flags, engine + runtime semantics) are unchanged is skipped on the next run and reported passed from the cache under build/bmc4j/verdict-cache/ — so "nothing changed" runs are near-free. Only green verdicts are ever cached; refuted/UNKNOWN proofs always re-run. Set false (or pass -Dbmc.noCache=true) to force full re-verification every time. The cache lives under build/, so gradlew clean clears it.

    • getAllowStubs

      public abstract org.gradle.api.provider.ListProperty<String> getAllowStubs()
      Build-wide acknowledged nondet stubs: methods every proof may rely on as havoc'd stand-ins without warning. JBMC stubs any callee it has no body for to a nondet result; bmc4j footnotes that on green proofs (and, under getStrictStubs(), turns an unacknowledged stub into UNKNOWN). Listing a method here silences it suite-wide; a proof can add more with @BmcProof(allowStubs = …). Entries are fully-qualified method names with an optional trailing wildcard: "java.util.Formatter.format", "java.util.Formatter.*", or "java.util.*".

    • getStrictStubs

      public abstract org.gradle.api.provider.Property<Boolean> getStrictStubs()
      Strict nondet-stub mode. When true, any unacknowledged stub a proof reaches turns its verdict into UNKNOWN (BmcUndecidedError) — nothing was proven wrong, but the verdict rests on havoc'd stand-ins, so it isn't trustworthy. Default false (lenient: green + footnote). Overridable at the command line with -Dbmc.strictStubs=true, so flipping it re-judges from the stored stub fact without re-running proofs (the stub list is cached).

    • getUserPackages

      public abstract org.gradle.api.provider.ListProperty<String> getUserPackages()
      Package prefixes of the module under test. A stub from one of these — the user's own code — is almost always a missing-dependency config bug, not a JDK modeling gap, so it is warned loudly even in lenient mode (and forces UNKNOWN in strict mode). Comma/space-separated prefixes, e.g. userPackages = ["com.acme"]. Overridable with -Dbmc.userPackages.

    • getModelSpec

      public abstract BmcExtensionConfig.ModelSpec getModelSpec()
      Registered user models with their declared intent. A class under src/bmcModel shadows its real counterpart on JBMC's analysis classpath; registering it here adds the trust metadata bmc4j needs to put provenance on a verdict that rests on it. 
      
 bmc {
     models {
         conformant("acme.FastList")                       // claims JDK fidelity
         domain("acme.NoCollisionMap", "keys are UUIDs, collision-free")  // intentional divergence
     }
 }

      A domain model encodes a constraint that deliberately diverges from the JDK -- it is Bmc.assume() at classpath altitude -- so it requires a one-line rationale, which is footnoted on every green proof that rests on it. A conformant model claims JDK fidelity and can be checked by the same conformance harness as bundled models. Under getStrictModels(), a model present under src/bmcModel but NOT registered here turns the verdict into UNKNOWN.

    • models

      public void models(org.gradle.api.Action<? super BmcExtensionConfig.ModelSpec> action)
      Configure the registered user models -- see getModelSpec().

    • getStrictModels

      public abstract org.gradle.api.provider.Property<Boolean> getStrictModels()
      Strict user-model mode, the strictStubs analog. When true, a model present under src/bmcModel with no bmc { models { ... } } intent declaration turns the proof's verdict into UNKNOWN (BmcUndecidedError) -- no proof silently rests on an undeclared override. Default false (lenient: green + a loud "UNDECLARED model" footnote). Overridable at the command line with -Dbmc.strictModels=true; like strictStubs it is read-time policy, so flipping it re-judges without re-running proofs.