GeezerVison

Copy link

Copy Markdown

Collaborator

CatarinaGamboa commented Oct 7, 2026

View reviewed changes

rcosta358 approved these changes Oct 7, 2026

View reviewed changes

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.

CatarinaGamboa added this pull request to stack #365 October 7, 2026 11:33

1 check passed

Fixes #334. **Stacked on #352** (compliance level 17, needed to parse
`try (r)`); retarget to `main` once #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#visitCtTryWithResource` scans resources → body →
a synthesized `r.close()` per resource (reverse declaration order, as
Java does) → catchers → finally. The close goes through the normal
invocation check, so it works for both `@StateRefinement` classes and
external refinements.

Errors are reported at the resource declaration (`Res r = new Res()`).
For a Java 9 resource reference they're reported at the `try (r)`
header.

**Spoon workaround:** Spoon 10.4.2 models `try (r)` as an *implicit*
copy of `r`'s declaration, initializer included. It is also repeated
once per earlier local named `r` in the file, so `try (r)` can yield
`[r, r, r]`. Scanning those would re-run `new 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 #334), use after the block, use in `catch`, and `try (r)` on an
already-closed `r`.
- `classes/try_with_resources_correct`: use inside, multiple resources,
`try (r)`, catch + finally.

`mvn test`: 369/369 pass.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

Follow-up to #352 (stacked on it; GitHub will retarget to `main` once
#352 merges).

## Problem
Spoon 10.4.2 bundles JDT 3.33, which only accepts compliance levels up
to 19 (`20` throws `Unrecognized option : -20`), so #352 has to cap the
level read from the project's pom at 19.

## Change
- `version.spoon`: 10.4.2 → **11.5.0** (JDT 3.46). It needs a Java 17+
runtime (class files are Java 17), which is fine since the verifier
already targets 20.
- `ComplianceLevel.MAX_SUPPORTED` (and so the default when no pom
declares a version): 19 → **26**, the highest level JDT 3.46 accepts
(`27` throws).

No source changes were needed for the Spoon API.

## Downstream
`vscode-liquidjava/server/pom.xml` declares `spoon-core` directly with
`version.spoon` = 10.4.2. That direct dependency overrides the
verifier's transitive one, so the server should be bumped to 11.5.0
together with the verifier version that includes this change. Otherwise
projects declaring Java 20+ would make the model builder throw there.

## Testing
`mvn test`: 369/369 pass (same as #352).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

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 <[email protected]>

Fixes #342 (regression tests only; no verifier change).

At the commit in the issue, `CommandLineLauncher` hard-coded compliance
level 8. Java 8 has no records, so JDT parsed the record header as a
method and its members as locals and a block; the real method was never
in the model. Spoon reports this as a warning in noclasspath mode, so
the run printed "Java compilation encountered issues" and then "Correct!
Passed Verification." It is already fixed on main by #352 (compliance
from the pom), #368 (default level 21, Spoon 11.5.0) and #370 (records
in the external-spec pass). Forcing level 11 or 15 still reproduces it;
16 and above report the error.

Fixtures, with the spec in its own file as in real projects:
- `classes/record_external_spec_error/`: State Refinement Errors in a
record's instance and static methods.
- `classes/record_external_spec_correct/`: the passing counterpart.

Related gaps found while investigating, not fixed here:
1. **A parse problem still ends in "Correct!" with only a warning.** If
Spoon's level is lower than the code needs, declarations can disappear
silently. `ComplianceLevel` reads only `maven.compiler.release`/`source`
properties of the nearest pom that has one, and ignores
`<release>`/`<source>` in the maven-compiler-plugin configuration, so a
parent property of 1.8 overridden in plugin config makes records vanish
again. Options: let that warning block the "Correct!" verdict, and read
the compiler-plugin config.
2. **One error hides later ones.** An error in a field initializer or
initializer block stops checking of the rest of the class (catch in
`visitCtClass`). `visitCtRecord` and `visitCtEnum` have no catch, so an
error in a record or enum static initializer reaches
`RefinementProcessor.processPackage` and later types in the package go
unchecked. Per-member catches like those in
`visitCtMethod`/`visitCtConstructor` would fix it.
3. **Test harness:** `TestExamples.matches` throws a
NullPointerException on a warning with no position (such as the
compilation warning).

Validation: `mvn test` passes all 412 tests (251 TestExamples cases).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

Fixes #388, fixes #389, fixes #390. Closes #344, closes #346, closes
#347.

When a class is not on the classpath (the usual case when one file of a
project is verified), Spoon leaves binary and unary operators without a
type and field references without a declaring type. The verifier then
crashed with a null dereference in `OperationsChecker` and
`Utils.qualifyFieldName`. This stopped verification on 25 of the 53
real-world files in #388.

An operation or field whose type cannot be resolved is now treated as
unrefined: comparisons and logical operators become an unknown boolean,
other operators carry no refinement, and `!` on an untyped operand is
boolean. Compound assignments such as `c += x.a()` take the same path.
An unknown value carries no information, so a refinement that depends on
one is reported as not provable rather than accepted. Violations next to
unresolved types are still reported.

#344, #346 and #347 already verify on main since the Spoon compliance
change (#352/#368) gives `var` locals their inferred type; this PR adds
regression fixtures for them.

Fixtures that import a missing package are excluded from javac
compilation in `liquidjava-example/pom.xml`
(`testSuite/**/*Unresolved*.java`); the verifier tests still read them
from source.

Known limits:
- A condition like `k > 0 && x.ok()` with an unresolved part becomes one
unknown boolean, so `k > 0` is not assumed inside the branch (possible
false errors, never missed ones).
- The #390 switch reproducer is checked by hand, not as a fixture: its
"Java compilation encountered issues" warning has no source position,
which `TestExamples` cannot handle.
- Pre-existing, unrelated to unresolved types: `p.x++` on another
object's field crashes, and `o.arr().length` gives a spurious "Invalid
refinement expression".

Validation: `mvn test` passes all 421 tests (260 TestExamples cases).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>