From a08c461d7f2099fc6922a022e1de8c1fbbfa6b90 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 22:50:22 +0000 Subject: [PATCH 1/2] OpenJML 21.0.29, drop the AtomicLong spec workaround; shared pins - formal-verification.yml: OpenJML 21.0.28 -> 21.0.29 (SHA-256 from the release asset digest). Measured locally: ESC 14/14 (1.7 s, SMT commands are pipelined now), RAC 285/285. - setup-openjml (fixups v2, new cache key): the AtomicLong.jml rm is gone, the upstream fix (OpenJML/Specs#29) shipped in 21.0.29 and the suite passes against the bundled file; ArrayDeque.jml is still broken and still deleted; the JAVA_VERSION repair is a no-op on 21.0.29, kept as a guard. - Class invariants re-tried as the bump checklist asks: the minimal reproducer runs clean on 21.0.29, but the four candidate invariants still break RAC on this class (NoSuchMethodError on SBOutputStream.JML$INV$$(), 106 errors, then a hang). They stay out; CLAUDE.md, TODO.md and the .jml note record the new symptom. - anthropics/claude-code-action v1.0.252 -> v1.0.255 (same commit in all four repositories), Gradle 9.8.1 -> 9.8.2 in the shared verify-signing-key-gradle job; shared-files.sha256 rewritten, including the scorecard.yml / osv-scanner.yml hashes Dependabot had left stale. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011CYhRUUCqwrHXPuEhS9W4M --- .github/actions/setup-openjml/action.yml | 26 +++++++++---------- .github/shared-files.sha256 | 10 +++---- .github/workflows/claude-code-review.yml | 2 +- .github/workflows/claude.yml | 2 +- .github/workflows/formal-verification.yml | 8 +++--- .github/workflows/publish.yml | 2 +- CHANGELOG.md | 6 +++++ CLAUDE.md | 23 +++++++++------- TODO.md | 18 ++++++++----- .../ladenthin/streambuffer/StreamBuffer.jml | 3 +++ 10 files changed, 60 insertions(+), 40 deletions(-) diff --git a/.github/actions/setup-openjml/action.yml b/.github/actions/setup-openjml/action.yml index a8497e3..2ee679f 100644 --- a/.github/actions/setup-openjml/action.yml +++ b/.github/actions/setup-openjml/action.yml @@ -27,9 +27,9 @@ runs: uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6 with: path: ${{ runner.temp }}/openjml - # spec-fixups-v1: bump this suffix whenever the fixup step below changes, + # spec-fixups-v2: bump this suffix whenever the fixup step below changes, # otherwise cached installs keep the previous fixup state. - key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v1 + key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v2 - name: Download pinned OpenJML (checksum-verified) if: steps.cache.outputs.cache-hit != 'true' @@ -44,31 +44,31 @@ runs: rm "$RUNNER_TEMP/openjml.zip" chmod +x "$RUNNER_TEMP/openjml/openjml" "$RUNNER_TEMP/openjml/openjml-java" - - name: Delete known-broken bundled JDK specs (fixups v1) + - name: Delete known-broken bundled JDK specs (fixups v2) if: steps.cache.outputs.cache-hit != 'true' shell: bash - # Both files ship broken in OpenJML 21.0.27 and 21.0.28 and break the RAC layer; deleting a + # The file ships broken in OpenJML 21.0.27 to 21.0.29 and breaks the RAC layer; deleting a # bundled spec degrades the affected JDK class to default (empty) contracts, which # is exactly what this repo needs — StreamBuffer's own contracts are the ones being - # checked. `rm` without -f: if an upgrade removes/fixes these files upstream, this + # checked. `rm` without -f: if an upgrade removes/fixes the file upstream, this # step fails loudly and the fixup (plus the cache-key suffix) must be revisited. # - ArrayDeque.jml: references the undeclared model variable `containsNull`; # `openjml --rac` fails with "cannot find symbol: containsNull". # Still open upstream (comment on OpenJML/OpenJML#806, closed issue). - # - concurrent/atomic/AtomicLong.jml: RAC-generated checks read the private field - # AtomicLong.value across the module boundary; every test touching the - # statistics counters then dies with java.lang.IllegalAccessError. - # Upstream fix: OpenJML/Specs#29 + OpenJML/OpenJML#982, merged into dev-21 on - # 2026-10-05, NOT in 21.0.28 (built from Specs 1a91cb6); drop this rm once released. + # Dropped in v2: concurrent/atomic/AtomicLong.jml, whose RAC-generated checks read the + # private field AtomicLong.value across the module boundary (IllegalAccessError in every + # test touching the statistics counters). The upstream fix (OpenJML/Specs#29 + + # OpenJML/OpenJML#982) shipped in 21.0.29 -- its contracts are `//-RAC@` there -- and the + # suite passes against the bundled file (285/285, measured 2026-10-20). run: | set -euo pipefail rm "$RUNNER_TEMP/openjml/specs/java/util/ArrayDeque.jml" - rm "$RUNNER_TEMP/openjml/specs/java/util/concurrent/atomic/AtomicLong.jml" - - name: Repair the bundled JDK release file (fixups v1) + - name: Repair the bundled JDK release file (fixups v2) if: steps.cache.outputs.cache-hit != 'true' shell: bash - # OpenJML 21.0.27's and 21.0.28's bundled jdk/release omit the JAVA_VERSION key. maven-surefire-plugin + # OpenJML 21.0.27's and 21.0.28's bundled jdk/release omit the JAVA_VERSION key (21.0.29 has + # it again, so this is a no-op there, kept as a guard against a regression). maven-surefire-plugin # reads that key to fingerprint a forked (SystemUtils.toJdkVersionFromReleaseFile); # without it the RAC job — which forks this exact JVM so the org.jmlspecs bigint runtime # class resolves — dies before any test with an NPE. Add the key if it is missing. diff --git a/.github/shared-files.sha256 b/.github/shared-files.sha256 index 78bc887..923aed0 100644 --- a/.github/shared-files.sha256 +++ b/.github/shared-files.sha256 @@ -55,11 +55,11 @@ e8f444ef851bd134330f1505f52b4b0970ef9a62dd76e4c25829241814ba5c73 .github/ISSUE_ 9a24b2a67ab8e6f52016093e9b6a89796adea29887b7820accede06cc0c0d170 .github/workflows/publish.yml#code-style 6e2ae11dad0616f66bbb2b6e6556f580bb987fd911d7132aa6bee2bfc7cc7b52 .java-version 71ec85b7a30e80b18a9ab1fac0199cc50d68548e6f00dd116ab0f904ad63aa50 .java-version.license -3f73b87c4675376cbe80f1fb914bd7020062dcdb9a7ee503d3ef787fd462358a .github/workflows/claude.yml -085f19495d9e0812dc90268ea7917579bd6eaf749c669a9f01922272a5cdf06f .github/workflows/claude-code-review.yml -463c34f6244675ee5bee3d28c28c84f5eb3c8bea4f45de3f6ce477348d29589c .github/workflows/scorecard.yml +30b3bed932fd05a34d79af0155166b548a7597e5ee4913aa105dd82a41d1936d .github/workflows/claude.yml +de1479c5c1e662c0f01d6afd0d18b4a71e8d8168b377287ca6e93285eef63358 .github/workflows/claude-code-review.yml +fe768632e9abc1a8cd39b038a77c1a79dbfd036129bb7f0d84b393251b369be6 .github/workflows/scorecard.yml 480afc0c1e41f3997b195d7297750b43599ba71a7471657aa32bfc9662b6fd30 .github/workflows/reuse.yml -cf75cdc06e5ab02359c12b6a8eecb97f2dd3d95502cd2b397d539584cefa56c3 .github/workflows/osv-scanner.yml +93aedaf67af1c4d63b2502107a51f2f454f2b3b4bc5f2fe892561e12363e57a9 .github/workflows/osv-scanner.yml 52182fe4073eb696606813d768ff9444e6b751978f9d27a8d84cc269e9f6cb3a .github/workflows/codeql.yml c9e757f2d0a2f456a08791697a94161c776d9b008a8aa75890da4133c81a99e9 .github/dependabot.yml f26d05f25a154b84d8f281bb92857811749e2225cdbc167362de930c48b532d1 .github/workflows/publish.yml#startgate @@ -67,6 +67,6 @@ e3dde66089fd568f03caeefee86ea36a9f6eb7f47e5dc6d053e0e5784fd7a208 .github/workfl 3ef45f189f4419e0d4087f572b3c1b6085c0fe39ac7979b07deb2e882f7ffe8c .github/workflows/publish.yml#verify-signing-key 09230b04c5f14bdda50a0c862152ff197a656cbc3fd0d110899c5f8150f8aa9a .github/workflows/publish.yml#check-snapshot 51e987d59efd9887b43e345edc0e0f3db21686879e3ca6ea9f0fdbc493d37121 .github/workflows/publish.yml#check-tag -06f0af70ed125dc5cc1506e27970059fb831971d3faaee56f868789f3282fdf9 .github/workflows/publish.yml#verify-signing-key-gradle +a4f42a0bfa9b14ca937675052b990e5f1dda238d762f9d0268ac282cd7030c0d .github/workflows/publish.yml#verify-signing-key-gradle c2684a3f93aaf552c13f845307536c2a14dda315c7d7b1e416bc66951b811dc1 .github/workflows/publish.yml#github-snapshot c09a030706dbea4221851ca0fcbfa6fc686165b408724724ade61724da6e123b .github/workflows/publish.yml#github-release diff --git a/.github/workflows/claude-code-review.yml b/.github/workflows/claude-code-review.yml index 3d7cc6e..f19ab4d 100644 --- a/.github/workflows/claude-code-review.yml +++ b/.github/workflows/claude-code-review.yml @@ -25,7 +25,7 @@ jobs: - name: Run Claude Code Review id: claude-review - uses: anthropics/claude-code-action@f27be6b65a4652f08a2ba3cff79114829b588967 # v1 + uses: anthropics/claude-code-action@e4a6faad497d33dbc7144135c75e41f82f0bf6c0 # v1 with: anthropic_api_key: ${{ secrets.ANTHROPIC_API_KEY }} prompt: | diff --git a/.github/workflows/claude.yml b/.github/workflows/claude.yml index 2588f38..1cbdb2b 100644 --- a/.github/workflows/claude.yml +++ b/.github/workflows/claude.yml @@ -36,7 +36,7 @@ jobs: - name: Run Claude Code id: claude - uses: anthropics/claude-code-action@f27be6b65a4652f08a2ba3cff79114829b588967 # v1 + uses: anthropics/claude-code-action@e4a6faad497d33dbc7144135c75e41f82f0bf6c0 # v1 with: anthropic_api_key: ${{ secrets.ANTHROPIC_API_KEY }} diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 4cbe5c9..d89f9f9 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -62,13 +62,13 @@ permissions: contents: read env: - OPENJML_VERSION: "21.0.28" - # SHA-256 of openjml-ubuntu-24.04-21.0.28.zip, taken from the GitHub release asset digest - # (https://github.com/OpenJML/OpenJML/releases/tag/21.0.28). ubuntu-latest is ubuntu-24.04, + OPENJML_VERSION: "21.0.29" + # SHA-256 of openjml-ubuntu-24.04-21.0.29.zip, taken from the GitHub release asset digest + # (https://github.com/OpenJML/OpenJML/releases/tag/21.0.29). ubuntu-latest is ubuntu-24.04, # matching the asset. When bumping the version: update both values, re-test the RAC spec # fixups in .github/actions/setup-openjml/action.yml, and re-try the class invariants noted # in src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml. - OPENJML_SHA256: "0a151820c4e680e32cb2e399a02615182c748fc24e308865b317783d4836df8a" + OPENJML_SHA256: "4fd633e1f555399e47bad8bbbe5ee1f4ae682dab74511ae9e4d7f0a10eeb914b" # The ESC scope: the complete static, sequential core of StreamBuffer. Every method listed # here MUST prove — and the count guard below additionally fails the job if the number of # completed proofs is not exactly ESC_EXPECTED_PROOFS, so a typo here (or a rename in the diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml index bea2626..c5e7d9a 100644 --- a/.github/workflows/publish.yml +++ b/.github/workflows/publish.yml @@ -153,7 +153,7 @@ jobs: distribution: temurin - uses: gradle/actions/setup-gradle@3f5f9adaf7d9fecd50b5935e54106014257a94e6 # v6 with: - gradle-version: "9.8.1" + gradle-version: "9.8.2" - name: Sign a throwaway artifact via useInMemoryPgpKeys (BouncyCastle) shell: bash env: diff --git a/CHANGELOG.md b/CHANGELOG.md index ebccf7f..25c1767 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -26,6 +26,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - **CI prints the runner's CPU** at the top of `test`, `vmlens` and the three formal-verification jobs (`.github/print-host-info.sh`, a shared file of the four repositories): Z3's proof times and the Lincheck and jcstress runs depend on it. +- Formal verification: OpenJML 21.0.29 (from 21.0.28). ESC 14/14 (1.7 s locally: SMT commands are now + pipelined) and RAC 285/285 unchanged. The `AtomicLong.jml` workaround is gone -- the upstream fix + (OpenJML/Specs#29) shipped in 21.0.29 -- while `ArrayDeque.jml` is still deleted at install. Class + invariants still break RAC (now `NoSuchMethodError` on the inner stream classes), so they stay out. +- Build tooling: `anthropics/claude-code-action` v1.0.255 (from v1.0.252) and Gradle 9.8.2 in the shared + `verify-signing-key-gradle` job, in step with the sibling repositories. - Formal verification: OpenJML 21.0.28 (from 21.0.27; default solver z3 5.1.0). ESC 14/14 and RAC 285/285 unchanged; the bundled-spec workarounds stay (the upstream fixes are not in 21.0.28). - **CI: shared files and the release gate are checked.** The files kept byte-identical with the sibling diff --git a/CLAUDE.md b/CLAUDE.md index 6bcd510..c89cca9 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -78,7 +78,7 @@ The `@GuardedBy("bufferLock")` lock discipline is gated separately by Error Pron build. The Checker Framework Lock Checker was evaluated as a further layer and deferred — see TODO.md "Formal verification". -**Local commands** (OpenJML 21.0.28, pinned in the workflow; native Windows builds exist since 21.0.27; +**Local commands** (OpenJML 21.0.29, pinned in the workflow; native Windows builds exist since 21.0.27; `` = unzipped release dir, `` = output of `mvn dependency:build-classpath -Dmdep.outputFile=... -DincludeScope=compile`): @@ -118,7 +118,11 @@ mvn -P jml-rac -Dopenjml.home= -Dopenjml.jdk.java=/jdk/bin/jav invariant inside the constructor of a non-static inner class and reads the field on the wrong class → `NoSuchFieldError` at runtime (14-line reproducer: private field + invariant + inner class). On this class every test fails (258/285). An earlier 21.0.27 compile crash - ("no enclosing instance") was not reproduced. Re-test on upgrades. + ("no enclosing instance") was not reproduced. **21.0.29 changed the symptom, not the defect:** + the 14-line reproducer runs clean there, but the four candidate invariants on this class still + break RAC -- `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$()` (RAC calls the + outer class's invariant check on the inner class), 106 errors before the suite hung in a + trim test (measured 2026-10-20). Re-test on upgrades. - `//@ nullable_by_default` at the class head is load-bearing for RAC: without it JML's non-null-by-default inserts an implicit non-null precondition on every reference parameter, so the null-argument tests hit `JmlAssertionError.Precondition` instead of the specified NPE. @@ -134,13 +138,14 @@ mvn -P jml-rac -Dopenjml.home= -Dopenjml.jdk.java=/jdk/bin/jav - RAC forks OpenJML's OWN JVM (`-Dopenjml.jdk.java`), because the bundled JDK library specs pull in `org.jmlspecs.lang.internal.bigint`, a class present only in OpenJML's patched JDK image. The setup action also patches `jdk/release` to add the `JAVA_VERSION` key surefire needs to - fork that JVM. -- Two bundled OpenJML JDK specs are known-broken and deleted at install time by - `.github/actions/setup-openjml` (`ArrayDeque.jml`: undeclared `containsNull`; - `atomic/AtomicLong.jml`: RAC reads the private field `value` → `IllegalAccessError`; - upstream fix [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) + test - [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982), merged into `dev-21`, - not yet released — still broken in 21.0.28). + fork that JVM (missing in 21.0.27/21.0.28, present again in 21.0.29; the guarded step is a no-op + there and stays as a regression guard). +- One bundled OpenJML JDK spec is known-broken and deleted at install time by + `.github/actions/setup-openjml` (`ArrayDeque.jml`: undeclared `containsNull`, still in 21.0.29). + The second one, `atomic/AtomicLong.jml` (RAC read the private field `value` → + `IllegalAccessError`), was fixed upstream by [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) + + [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982), released in 21.0.29; its + `rm` is gone, and the suite passes against the bundled file (285/285). - RAC classes are class-file 65 and live only under `target/rac-classes` — they never enter the shipped jar, so the Java 8 bytecode floor is unaffected. diff --git a/TODO.md b/TODO.md index 530a7e7..359ca49 100644 --- a/TODO.md +++ b/TODO.md @@ -34,16 +34,17 @@ annotated, so everything below is genuinely still open. reporting upstream (its native peer already implements the methods the stub model never declared). Possible extension: a second harness for the array-read / `waitForAtLeast` blocking paths (jcstress already covers those; JPF would make them exhaustive too). - - **OpenJML bundled-spec defects** (pinned 21.0.28 still ships all of them; it was built from - Specs `1a91cb6`, before the fixes below). All three share one cause: a model field declared + - **OpenJML bundled-spec defects** (21.0.28 shipped all of them, built from Specs `1a91cb6`; + the pinned 21.0.29 carries the AtomicLong fix and still ships the ArrayDeque one). All three share one cause: a model field declared only behind `-RAC` in `java/lang/Iterable.jml` (`values`, `containsNull`) or a private `java.base` field (`value`) used in a clause RAC compiles. - `atomic/Atomic{Long,Integer,Boolean}.jml` (`value` → `IllegalAccessError` at runtime): - **fixed upstream, unreleased.** [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) + **fixed upstream, released in 21.0.29** (its contracts are `//-RAC@` there). [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) (`4ebda9c`) + maintainer extension `c365293` on Specs `dev-21`; testspecs [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982) merged into `dev-21` (2026-10-05). Verified: streambuffer RAC 285/285 with the fixed spec, 258/285 without. - Once released: drop the `AtomicLong.jml` `rm` in `.github/actions/setup-openjml`. + **Done 2026-10-20:** the `AtomicLong.jml` `rm` is gone from `.github/actions/setup-openjml` + (fixups v2); RAC 285/285 against the bundled 21.0.29 file. - `java/util/ArrayDeque.jml:30` (`containsNull` → RAC compile error) and `java/util/Collections.jml:116-117` (`singletonList`, `values` → RAC compile error): **open.** Both are the original errors of the closed @@ -53,11 +54,16 @@ annotated, so everything below is genuinely still open. [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012) (2026-10-07). Fix + red/green testspecs cases prepared locally, offered as PRs. Once released: drop the `ArrayDeque.jml` `rm`. - - Missing `JAVA_VERSION` key in the bundled `jdk/release`: still missing in 21.0.28 - (reported in #1012). + - Missing `JAVA_VERSION` key in the bundled `jdk/release`: missing in 21.0.28 (reported in #1012), + **present again in 21.0.29**; the guarded repair step is a no-op there and stays as a guard. - **Invariants + non-static inner classes break RAC — confirmed OpenJML bug, reported in [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012).** RAC checks the outer class's invariant inside the inner class's constructor and reads the field on the inner class → `NoSuchFieldError` at runtime (21.0.27 and 21.0.28). + **21.0.29: the minimal reproducer below runs clean, the defect on this class does not go away** -- + with the four candidate invariants RAC throws `NoSuchMethodError` on + `StreamBuffer$SBOutputStream.JML$INV$$()` (the outer invariant check called on the inner + class), 106 errors, then the suite hangs in a trim test (measured 2026-10-20). A reproducer for + #1012 therefore needs an inner class whose methods run while the outer invariant is checked. Minimal reproducer: ```java public class Outer { diff --git a/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml b/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml index cc33930..2a362ba 100644 --- a/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml +++ b/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml @@ -88,6 +88,9 @@ public class StreamBuffer implements Closeable { // NoSuchFieldError ("SBInputStream does not have member field 'long availableBytes'"); // 258/285 tests fail. Minimal reproducer: private field + invariant + inner class (see // TODO.md). An earlier 21.0.27 compile crash ("no enclosing instance") was not reproduced. + // 21.0.29: the minimal reproducer passes, but these four invariants on this class still break + // RAC with NoSuchMethodError on SBOutputStream.JML$INV$$() (106 errors, then a hang in a + // trim test) -- the same defect with a different symptom. // The candidate invariants // (0 <= availableBytes, 0 <= positionAtCurrentBufferEntry, 1 <= maxAllocationSize, // 0 <= maxObservedBytes) would have been RAC-only value anyway — the ESC layer proves From 90e730af0cef645fe675303e00c9bd9d86634c7c Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 22:53:40 +0000 Subject: [PATCH 2/2] Drop the "hang" from the invariant re-test note The stall seen while re-trying the class invariants is most likely OpenJML/OpenJML#1050 (a stack trace per call for skipped specification clauses; fixed on dev-21, not yet in 21.0.29), not part of the invariant defect, so the notes record only the NoSuchMethodError and its count. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011CYhRUUCqwrHXPuEhS9W4M --- CLAUDE.md | 3 +-- TODO.md | 2 +- src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml | 4 ++-- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index c89cca9..c003a7c 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -121,8 +121,7 @@ mvn -P jml-rac -Dopenjml.home= -Dopenjml.jdk.java=/jdk/bin/jav ("no enclosing instance") was not reproduced. **21.0.29 changed the symptom, not the defect:** the 14-line reproducer runs clean there, but the four candidate invariants on this class still break RAC -- `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$()` (RAC calls the - outer class's invariant check on the inner class), 106 errors before the suite hung in a - trim test (measured 2026-10-20). Re-test on upgrades. + outer class's invariant check on the inner class), 106 errors (measured 2026-10-20). Re-test on upgrades. - `//@ nullable_by_default` at the class head is load-bearing for RAC: without it JML's non-null-by-default inserts an implicit non-null precondition on every reference parameter, so the null-argument tests hit `JmlAssertionError.Precondition` instead of the specified NPE. diff --git a/TODO.md b/TODO.md index 359ca49..58399f0 100644 --- a/TODO.md +++ b/TODO.md @@ -62,7 +62,7 @@ annotated, so everything below is genuinely still open. **21.0.29: the minimal reproducer below runs clean, the defect on this class does not go away** -- with the four candidate invariants RAC throws `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$()` (the outer invariant check called on the inner - class), 106 errors, then the suite hangs in a trim test (measured 2026-10-20). A reproducer for + class), 106 errors (measured 2026-10-20). A reproducer for #1012 therefore needs an inner class whose methods run while the outer invariant is checked. Minimal reproducer: ```java diff --git a/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml b/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml index 2a362ba..f6ba247 100644 --- a/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml +++ b/src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml @@ -89,8 +89,8 @@ public class StreamBuffer implements Closeable { // 258/285 tests fail. Minimal reproducer: private field + invariant + inner class (see // TODO.md). An earlier 21.0.27 compile crash ("no enclosing instance") was not reproduced. // 21.0.29: the minimal reproducer passes, but these four invariants on this class still break - // RAC with NoSuchMethodError on SBOutputStream.JML$INV$$() (106 errors, then a hang in a - // trim test) -- the same defect with a different symptom. + // RAC with NoSuchMethodError on SBOutputStream.JML$INV$$() (106 errors) -- the same + // defect with a different symptom. // The candidate invariants // (0 <= availableBytes, 0 <= positionAtCurrentBufferEntry, 1 <= maxAllocationSize, // 0 <= maxObservedBytes) would have been RAC-only value anyway — the ESC layer proves