GeezerVison

Fixes #337, fixes #340.

Two false negatives found in the real-code examples, one commit each.

#337: state changes through an alias. Res b = a; records b == a, but b.close() gave b a new closed version that was no longer equal to a, so a.read() passed. After a state change, every other variable of a related type that the solver proves refers to the same object now points to the new version (AuxStateHandler.updateAliases, relatedTypes). Reassigning b = new Res() breaks the alias, so closing b afterwards leaves a alone.

Fixtures: ErrorStateChangeThroughAlias (plain alias, alias of an alias, alias created by a later assignment, close inside an if) and CorrectStateChangeThroughAlias (separate objects, reassignment, state-preserving calls, closing through either name in different branches).

#340: a mutable field read as its initializer. A field initializer's value stayed visible in every method. When a method (not a constructor) starts, each non-final field now keeps only its declared refinement (RefinementTypeChecker.forgetMutableFieldValues). Final fields keep their initializer, and assignments within the method are still tracked.

Fixtures: ErrorMutableFieldInitializer (the reproducer via q and this.q, a static non-final field, a non-final field holding an object with a state) and CorrectMutableFieldInitializer (final field, field refinement that guarantees the bound, assign-then-read, read in the constructor).

Existing fixtures changed: three field cases in CorrectDeferredCallbackState / ErrorDeferredCallbackState relied on a non-final field's initializer state inside a method. Their calls moved into the constructors, where that state really holds, so they still test that creating a callback does not run it.

Not covered:

• Aliasing through method arguments: parameter state is unknown and callee state changes are not propagated to the caller.
• Variables that may or may not alias (e.g. two parameters) still keep separate states.
• updateGhostField (state-tracked int field writes) does not update aliases.
• A final field holding an object with a state still assumes its initializer state, although another method can change it. Treating it like a non-final field breaks classes/state_field_initializer_correct (Fix Field Initialization #281), so it needs a design decision.
• Within one method, a call that may write a field (this.setQ(x)) does not invalidate the value assigned earlier in the method (pre-existing).

Validation: mvn test passes all 414 tests (253 TestExamples cases).

🤖 Generated with Claude Code