Index

A B C D G M O R
All Classes and Interfaces|All Packages

A

apply(Project) - Method in class org.bmc4j.gradle.BmcPlugin

B

BmcExtensionConfig - Class in org.bmc4j.gradle

The bmc { } DSL block.

BmcExtensionConfig() - Constructor for class org.bmc4j.gradle.BmcExtensionConfig

BmcExtensionConfig.ModelSpec - Class in org.bmc4j.gradle

The models { conformant(...) / domain(...) } DSL block.

BmcPlugin - Class in org.bmc4j.gradle

Wires bounded model checking into a JVM project.

BmcPlugin() - Constructor for class org.bmc4j.gradle.BmcPlugin

BmcStubReportTask - Class in org.bmc4j.gradle

Aggregates the nondet stubs harvested across the proof suite into a ranked "most-hit unmodeled methods" report — a data-driven bmc-models backlog.

BmcStubReportTask() - Constructor for class org.bmc4j.gradle.BmcStubReportTask

C

conformant(String) - Method in class org.bmc4j.gradle.BmcExtensionConfig.ModelSpec

Register a conformant user model (claims JDK fidelity).

D

domain(String, String) - Method in class org.bmc4j.gradle.BmcExtensionConfig.ModelSpec

Register a domain user model (intentional divergence).

G

getAllowStubs() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Build-wide acknowledged nondet stubs: methods every proof may rely on as havoc'd stand-ins without warning.

getCache() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Per-proof verdict caching.

getCacheDir() - Method in class org.bmc4j.gradle.BmcStubReportTask

The verdict-cache directory to scan (build/bmc4j/verdict-cache); set by the plugin.

getEntries() - Method in class org.bmc4j.gradle.BmcExtensionConfig.ModelSpec

Serialized declarations, one per entry as intent|fqn|rationale; joined by the plugin.

getJbmcPath() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Optional path to an existing JBMC binary.

getModelSpec() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Registered user models with their declared intent.

getParallelism() - Method in class org.bmc4j.gradle.BmcExtensionConfig

How many proofs to verify concurrently — each runs its own jbmc process, and proofs are independent, so this scales near-linearly.

getProgress() - Method in class org.bmc4j.gradle.BmcExtensionConfig

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.

getReportFile() - Method in class org.bmc4j.gradle.BmcStubReportTask

Where the ranked report is written.

getSolver() - Method in class org.bmc4j.gradle.BmcExtensionConfig

SAT/SMT backend for JBMC.

getSolverCmd() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Path/command for an external SMT2 solver binary (used with --smt2); overrides BmcExtensionConfig.getSolver().

getSolverPath() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Directory holding the SMT solver binary (e.g.

getStrictModels() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Strict user-model mode, the strictStubs analog.

getStrictStubs() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Strict nondet-stub mode.

getTimeoutSeconds() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Default per-proof wall-clock budget in seconds.

getUnwind() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Default loop/recursion unwinding bound for proofs that don't override it.

getUserPackages() - Method in class org.bmc4j.gradle.BmcExtensionConfig

Package prefixes of the module under test.

M

models(Action<? super BmcExtensionConfig.ModelSpec>) - Method in class org.bmc4j.gradle.BmcExtensionConfig

Configure the registered user models -- see BmcExtensionConfig.getModelSpec().

ModelSpec() - Constructor for class org.bmc4j.gradle.BmcExtensionConfig.ModelSpec

O

org.bmc4j.gradle - package org.bmc4j.gradle

R

report() - Method in class org.bmc4j.gradle.BmcStubReportTask

A B C D G M O R
All Classes and Interfaces|All Packages