Nested classes wipe the outer class's field refinements
Maintainer antworten meist innerhalb von 2 Tagen
Dieses Issue hat noch niemand übernommen.
Bewertung
- Schwierigkeit
- 4/5
- Geschätzter Aufwand
- 3-5 Tage
- Anfängerfreundlichkeit
- 55/100
Rechercherichtung
Start in RefinementTypeChecker.visitCtClass and MethodsFirstChecker.visitCtClass, focusing on how context.reinitializeContext() changes ctxVars while Spoon visits nested classes. Use the OuterWiped reproducer to verify that the outer field refinement remains available after Inner, while writes such as x = -1 are still rejected. Done means the reproducer passes verification without losing the existing write check.
Vom Indexierungsmodell aus dem Issue-Text verfasst.
Beschreibung
Description
Entering a nested class resets the variable context, which wipes the outer class's fields. Any method of the outer class declared after a nested class loses the refinements of the outer class's own fields.
Minimal reproducer
import liquidjava.specification.Refinement;
public class OuterWiped {
@Refinement("_ > 0") int x = 1;
static class Inner { int y; }
@Refinement("_ > 0")
public int get() { return x; }
}
Expected
Correct! Passed Verification.
Actual
Refinement Error: true is not a subtype of #ret¹ > 0
6 | public int get() { return x; }
| ^^^^^^^^^
--> Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.
Removing Inner (or moving it below get) makes it pass. Writes such as x = -1 are still rejected correctly, because the expected refinement is read from the field's annotation.
Cause
RefinementTypeChecker.visitCtClass (and MethodsFirstChecker.visitCtClass) call context.reinitializeContext(), which clears ctxVars. Spoon visits nested classes as children of the outer class, so visiting Inner clears this#x. The opposite also happens: the nested class's fields stay in the context after it returns. That leak is why declaring a nested class before its use works today (see #308).
Possible fix
When a class is entered, register all of its fields (and those of its nested types) before visiting any methods, and keep nested classes from clearing the enclosing class's context. This would probably also fix the read case above.
Reproduced on main at fbfb4e23 (liquidjava-verifier 0.0.35).
- Vorherrschende Sprache
- Java
- Sterne
- 67
- Forks
- 36
- Ø Merge
- 3 T. 16 Std.
- Gemergte PRs (30 T.)
- 9
Entwicklungsumgebung
- Kein Dockerfile und keine Docker-Compose-Datei
- Hat eine Pull-Request-Vorlage
- Beitragsleitfaden lesen
Erste Schritte
- Lesen Sie das ganze Issue und danach den Beitragsleitfaden des Projekts.
- Schreiben Sie ins Issue, dass Sie es übernehmen — das erspart doppelte Arbeit.
- Forken Sie das Repository und arbeiten Sie in einem Branch.
- Öffnen Sie einen Pull Request, der die Issue-Nummer nennt.
Mehr aus liquid-java/liquidjava
-
bug
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 78/100
liquid-java/liquidjava#321 ·
Maintainer antworten meist innerhalb von 2 Tagen
-
Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 68/100
liquid-java/liquidjava#323 ·
Maintainer antworten meist innerhalb von 2 Tagen
-
Soundness: a field of another class or object is read as this class's field with the same nameOffenbug
Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 76/100
liquid-java/liquidjava#322 ·
Maintainer antworten meist innerhalb von 2 Tagen
-
bug
Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 52/100
liquid-java/liquidjava#318 ·
Maintainer antworten meist innerhalb von 2 Tagen
-
bug
Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 62/100
liquid-java/liquidjava#316 ·
Maintainer antworten meist innerhalb von 2 Tagen
Alle Issues in liquid-java/liquidjava
Ähnliche Issues
-
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 78/100
objectionary/eo#9182 ·
Maintainer antworten meist innerhalb von 1 Tag
-
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 88/100
objectionary/hone-maven-plugin#1293 ·
Maintainer antworten meist innerhalb von 1 Tag
-
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 88/100
Maintainer antworten meist innerhalb von 1 Tag
-
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 88/100
MaikuB/flutter_appauth#683 ·
-
wait for review
Schwierigkeit 1/5 1-3 Stunden Anfängerfreundlichkeit 90/100
Maintainer antworten meist innerhalb von 1 Tag