[bernardladenthin]

Summary

• Four library fixes from the bug hunt (44 commits; ids, reproductions and red/green tests in BUGHUNT-FOUND.md): safeWrite could be bypassed by a concurrent write(int) (the instance-wide clone flag is gone, cloning is a parameter of the private write path; F02); a concurrent trim() let a reader see a half-emptied buffer (it now copies straight from the FIFO into blocks of at most maxAllocationSize and leaves the count unchanged; F73); a write racing close() could land after the close (the closed check runs under bufferLock, close() sets the flag under the same lock and waits for a write or trim in progress; F149); a trim() whose block allocation failed with an OutOfMemoryError lost the bytes it had already copied while available() still counted them -- every block is now allocated before the FIFO is touched, through the one package-private seam allocateTrimChunk(int), which is how the test provokes the failure (F268). The statistics count the I/O of a trim start signal (F212), and the clampToMaxInt Javadoc and the maxAllocationSize default are corrected (F110).
• Tests that could pass without checking anything are tightened: the jqwik properties now run in every build (their class name matched none of Surefire's include patterns), the concurrent safeWrite test surfaces background failures, a test that never reached the buffer is removed, a new test pins that close() waits for a write on another thread, a jcstress WriteRacingCloseRace is added, and the close-during-trim tests describe the current trim().
• Formal verification: a third JPF harness (WriteClose.jpf, writer, closer and reader in three threads) model-checks the order of write and close, which the existing harness cannot see; under RAC the two stress loops and the jqwik tries are scaled down (RAC: spurious ClassCastException from a callee's signals clause at the call site, and a stack trace per call for skipped Arrays.equalArrays clauses (from streambuffer) OpenJML/OpenJML#1050 prints a stack trace per System.arraycopy), and the two suspected OpenJML RAC defects are recorded with their upstream reference.
• Docs: read(byte[], off, len) waiting for all len bytes is now stated in the Javadoc and the README, with the waitForAnyData() + available() pattern; the trim signals are documented as released under the buffer lock (a release() must not wait for this buffer), and the README's maxAllocationSize section says what happens when an allocation fails during a trim.
• The branch carries main (PR Drop the ArrayDeque spec workaround, OpenJML 21.0.29 has the fix #188 merged into it, conflicts in CHANGELOG.md / CLAUDE.md resolved by keeping both sides' entries).

Test plan

• Affected unit / integration tests pass locally: StreamBufferTest, StreamBufferProperties, StreamBufferLincheckTest (307/307), PIT 198/198 (mutationThreshold held), spotbugs:check, spotless:check, the javadoc jar; the OpenJML ESC/RAC and JPF jobs run in the separate formal-verification workflow.
• CI is green on this branch (head 1204a58: Build, Test, vmlens, Report/PIT, smoke, shared files, code style, OpenJML ESC + RAC, CodeQL, osv; the two GPG jobs are red by design on a non-main branch, SonarCloud's single finding on positionAtCurrentBufferEntry += toCopy is a false positive -- the update runs under bufferLock).
• Docs / CHANGELOG updated: CHANGELOG.md, README.md, CLAUDE.md, TODO.md, src/test/jpf/README.md, BUGHUNT-FOUND.md / BUGHUNT-CHECKED.md.

Related issues / PRs

• Refs RAC: spurious ClassCastException from a callee's signals clause at the call site, and a stack trace per call for skipped Arrays.equalArrays clauses (from streambuffer) OpenJML/OpenJML#1050 (the RAC stack traces behind the scaled-down loops).
• Sibling PRs of the same branch: java-llama.cpp, BitcoinAddressFinder, srcmorph and workspace (the bug-hunt loop and its learnings).

Checklist

• I have read CONTRIBUTING.md and CODE_OF_CONDUCT.md
• My commits follow Conventional Commits -- they are imperative one-line subjects in the repository's existing style, not type(scope): prefixed.
• No security-sensitive changes

---

Generated by Claude Code

[coveralls]

Coverage is 100.0% — ccr-90fc5f6a-vs4s0f into main. No base build found for main.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 98.89%. Comparing base (920fc7d) to head (1204a58).
⚠️ Report is 1 commits behind head on main.

Additional details and impacted files

@@             Coverage Diff              @@
##               main     #189      +/-   ##
============================================
+ Coverage     96.99%   98.89%   +1.90%     
- Complexity      116      119       +3     
============================================
  Files             1        1              
  Lines           266      271       +5     
  Branches         29       28       -1     
============================================
+ Hits            258      268      +10     
+ Misses            2        0       -2     
+ Partials          6        3       -3     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

[sonarqubecloud]

Quality Gate failed

Failed conditions
C Reliability Rating on New Code (required ≥ A)

See analysis details on SonarQube Cloud

Catch issues before they fail your Quality Gate with our IDE extension SonarQube for IDE