Repository navigation
Model the implicit close() of try-with-resources - #358
Merged
Merged
Conversation
Collaborator
Author
|
This looks good! Once we update the versions of spoon/java we might need to consider more cases but probably through the same strategy |
CatarinaGamboa
added this pull request to stack #365
October 7, 2026 11:33
Check `r.close()` for each resource when the try body ends, in reverse declaration order and before catch/finally, so typestate errors from the implicit close (double close, use after the block) are reported. Java 9 resource references (`try (r)`) are modelled by Spoon 10.4.2 as an implicit copy of r's declaration (initializer included), repeated once per earlier local with the same name; these are not scanned and closed once. Fixes #334 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa
force-pushed
the
fix/334-twr-close
branch
from
October 7, 2026 11:35
869ac9a to
3c29de4
Compare
CatarinaGamboa
added a commit
that referenced
this pull request
Oct 8, 2026
Redoes #363, which was merged into `fix/compliance-level` after that branch had already been merged into `main` (#352), so `main` is still on Spoon 10.4.2. ## Change - `version.spoon`: 10.4.2 → **11.5.0** (JDT 3.46). Its class files target Java 17, so it runs on our Java 20 build. - `ComplianceLevel`: the cap goes from 19 to **26** (highest level JDT 3.46 accepts; `27` throws), and a separate `DEFAULT` of **21** is used when no pom declares a Java version (it used to be the cap). - `RefinementTypeChecker#visitCtTryWithResource` (from #358): in Spoon 11, `CtResource` is no longer a `CtVariable`. A resource is now either a `CtLocalVariable` (`try (R r = ...)`) or a `CtVariableRead` (Java 9 `try (r)`). Spoon 10 modelled `try (r)` as an implicit copy of `r`'s declaration, repeated per earlier same-named local. That workaround (skip implicit copies, dedupe by name, header position) is gone: every resource is scanned and closed once, and the implicit `close()` is built from the declaration's reference or a clone of the read, positioned at the resource. ## Downstream `vscode-liquidjava/server/pom.xml` declares `spoon-core` 10.4.2 directly, which overrides the verifier's version. Bump it to 11.5.0 together with the verifier release that includes this. ## Testing `mvn test`: 379/379 pass, including `try_with_resources_correct` / `try_with_resources_error` (both resource forms) and `CorrectModernJavaSyntax`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #334. Stacked on #352 (compliance level 17, needed to parse
try (r)); retarget tomainonce #352 merges.Problem
The
close()Java inserts at the end of a try-with-resources block was never checked, so a double close or a use after the block passed verification.Change
RefinementTypeChecker#visitCtTryWithResourcescans resources → body → a synthesizedr.close()per resource (reverse declaration order, as Java does) → catchers → finally. The close goes through the normal invocation check, so it works for both@StateRefinementclasses and external refinements.Errors are reported at the resource declaration (
Res r = new Res()). For a Java 9 resource reference they're reported at thetry (r)header.Spoon workaround: Spoon 10.4.2 models
try (r)as an implicit copy ofr's declaration, initializer included. It is also repeated once per earlier local namedrin the file, sotry (r)can yield[r, r, r]. Scanning those would re-runnew Res()and reset the state, so implicit resources are not scanned and are closed once per name.Tests
classes/try_with_resources_error: double close (both reproducers from Soundness: the implicitclose()of try-with-resources is not modelled #334), use after the block, use incatch, andtry (r)on an already-closedr.classes/try_with_resources_correct: use inside, multiple resources,try (r), catch + finally.mvn test: 369/369 pass.🤖 Generated with Claude Code