[CatarinaGamboa]

Four crashes found by verifying single files of real projects, where the project's other classes and its dependencies are not on the classpath. One commit per cause (#425 and #396 share one).

1. A variable whose type cannot be resolved (#425, #396)

import org.example.missing.Cookie;
void createAll(Cookie[] cookies) {
    for (int i = 0; i < cookies.length; i++) cookies[i].create();     // #425
}
request.names().forEach(name -> System.out.println(name));            // #396, Request not on the classpath

NullPointerException: Cannot invoke "CtTypeReference.getSuperclass()" because "type" is null
  at Context.addVarToContext

Spoon leaves the type of the array element, and of a lambda parameter whose target type is unknown, unset. Context looks up the supertypes of every variable it adds. Skipping that lookup for null types is not enough: the null type then crashes the SMT translation (TranslatorContextToZ3, type.isEnum()) as soon as the variable is part of a query (e.g. any(cookies[0]) with a refined parameter). Fix: Context.addVarToContext and addInstanceToContext type such a variable as Object, so it has no supertypes and carries no information. I also removed a supertype lookup in addVarToContext that ran twice (the overload it calls already does it).

2. A write to a field declared outside the analyzed sources (#426)

import org.example.missing.Options;
opts.sampleSize = 1;      // also opts.sampleSize += 1, and java.awt.Point p; p.x = 3

NullPointerException: Cannot invoke "CtElement.getAnnotations()" because "element" is null
  at TypeChecker.getRefinementFromAnnotation
  at TypeChecker.checkVariableRefinements

The field has no declaration, either because its class is not on the classpath or because it is a library field (Point.x crashed too). Fix: at the field-write call site, the write itself stands in for a missing declaration. It has no refinement annotations, so the write is checked like a write to an unrefined field. The ghost field update after a field write now only runs for fields declared in the analyzed sources: they are the only ones that have a ghost, and updateGhostField dereferences the declaration. Two supertype lookups that AuxStateHandler repeated after addInstanceToContext are removed: addInstanceVariable already does them, and they would throw on an unresolved type.

3. A for loop whose body is an empty statement (#395)

for (int i = 0; i < counts.length; total += counts[i], i++)
    ;

NullPointerException: Cannot invoke "CtStatement.getElements(Filter)" because the return value of "CtFor.getBody()" is null

Fix: visitCtFor treats a missing body as an empty one. The condition and the update are still checked. while, do and for-each loops with ; as their body already verified.

Tests

• CorrectUnresolvedArrayElement, CorrectUnresolvedLambdaParameter: the issue reproducers, plus an element passed to a refined parameter, so it reaches the SMT query. All crashed before.
• ErrorUnresolvedArrayElement, ErrorUnresolvedLambdaParameter: a violation after the unresolved construct, in the same method, is still reported.
• CorrectUnresolvedFieldWrite (=, +=, and Point.x) and ErrorUnresolvedFieldWrite.
• CorrectEmptyLoopBody (for, while, do, for-each with ; as the body, plus a refined counter) and ErrorEmptyLoopBody (a for update that breaks a refinement is still reported).
• mvn test: 504 tests, 0 failures.

Results on real files

We ran the 53 real-world files from #388 (74 with the fixed versions, each verified on its own) on main (4a89df6) and on this branch:

	crash	error reported	passed
main	20 (15 of the 53 originals)	43	11
this PR	1	60	13

• 14 of the 15 crashes on the 53 originals are fixed, and all 5 on the fixed versions. The remaining crash is GCIS-125 GuessingGameServer: the file itself does not parse (if (socket.) followed by a commented-out body).
• The 54 files that did not crash give exactly the same output as before.
• Of the 19 files that no longer crash, 17 now report diagnostics and 2 pass. These diagnostics were hidden by the crash. They are expected bug reports (e.g. the Throwable initCause and BufferedReader typestate bugs at their recorded lines) or limitations that main already shows on other files, in code without unresolved types: Invalid refinement expression on char literals, ~ and .length (False error: a[i].length is rejected as an invalid refinement expression #348), Sorts Int and Bool are incompatible on new InetSocketAddress(...), Not Found Error: Constant 'X.Y' could not be found on a constant of an unresolved class (main gives the same), and an Error: null when the result of an unresolved call is passed to a refined parameter (reproduced on main without this PR).
• The 2 files that now pass (Delos Gorgoneion, OpenMetadata PersonaContextBuilder) contain an initCause bug on an exception class that is not on the classpath. Its supertypes, including Throwable, are unknown, so the Throwable spec cannot apply.

Known limits:

• When a lambda's target type cannot be resolved, JDT does not resolve the lambda's body, so violations inside it are not reported (request.names(() -> positive(0)) passes on main too).
• obj.f++ on a field of another object crashes on main as well, with or without unresolved types (a.y++, p.x++, -a.y). It will be handled separately.
• A write to a refined field of this file reached through an unresolved expression (s.getA().f = -1) is now not checked: its declaring type is unknown. Main crashed there.

Closes #425, #426, #396, #395.

🤖 Generated with Claude Code

[CatarinaGamboa]

[Codex review] I checked the unresolved-type fallback at both variable insertion points, the missing field-declaration path for assignments, and the null body handling in visitCtFor. The new examples exercise the subsequent SMT query and a later violation, which guards against merely hiding the crash. The verifier suite passes locally at this head (./mvnw -q -pl liquidjava-verifier -am test). I found no additional issue within this PR's stated scope.

[CatarinaGamboa]

[Claude] Thanks for checking. No changes needed.