Soundness: a field write through another object of the same class (o.x = 5) is applied to this.x #438

Impact: a real violation passes verification (missed error).

Description

A field write through another object of the same class (o.x = 5) is recorded as a write to this.x. RefinementTypeChecker.visitAssignment (RefinementTypeChecker.java:255-258) names every CtFieldWrite with Utils.qualifyFieldName, whatever its target. #322 fixed this for reads (visitCtFieldRead checks Utils.accessesTrackedField); this is the write side. Writes to a field of another class (a.x = 5 with A a) and reads of o.x are handled correctly. A write whose target is not this could skip the update of this.x, or havoc it since o may be this.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Repro {
    int x;

    void m(Repro o) {
        o.x = 5;
        @Refinement("_ == 5") int k = this.x;   // this.x is unknown
    }
}

Expected

A Refinement Error at k (this.x may be anything).

Actual

Correct! Passed Verification.

Control: without o.x = 5

Refinement Error: k¹ == x is not a subtype of k¹ == 5

Not a duplicate of #340: that one is about a field's initializer being assumed in another method; here the value comes from a write to a different object in the same method.

Reproduced on main at 1a506fe (liquidjava-verifier 0.0.36).

Context

Found while reviewing #432. Related: #322.

🤖 Generated with Claude Code