GeezerVisonThe World Wide Web, restored to 800 pixels of glory. |
| Home|About|Gaming cabinet|Archives|How it works|Starter sites |
GeezerVison is showing github.com — Soundness: a call inside an anonymous class body changes the field state seen by other methods · Issue #341 · liquid-java/liquidjava Closed Labels bugSomething isn't workingSomething isn't working DescriptionImpact: a real bug passes verification (false negative). It blocks 1 of the 48 real-code examples we built (bugs mined from open-source Java). Description A state-changing call on a field, made inside an anonymous class's method (here a listener that may never run), is applied to the field's state as if it ran in the constructor, so Minimal reproducer import javax.swing.undo.UndoManager; import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; @ExternalRefinementsFor("javax.swing.undo.UndoManager") @StateSet({"empty", "full"}) interface UndoManagerRefinements { @StateRefinement(to = "empty(this)") void UndoManager(); @StateRefinement(to = "full(this)") boolean addEdit(javax.swing.undo.UndoableEdit anEdit); @StateRefinement(from = "full(this)") void undo(); } public class Repro { UndoManager undoManager = new UndoManager(); public Repro() { Runnable listener = new Runnable() { public void run() { undoManager.addEdit(null); } }; } public void undo() { undoManager.undo(); } } Expected A state error at Actual Control: the same code without the problem construct is reported import javax.swing.undo.UndoManager; import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; @ExternalRefinementsFor("javax.swing.undo.UndoManager") @StateSet({"empty", "full"}) interface UndoManagerRefinements { @StateRefinement(to = "empty(this)") void UndoManager(); @StateRefinement(to = "full(this)") boolean addEdit(javax.swing.undo.UndoableEdit anEdit); @StateRefinement(from = "full(this)") void undo(); } public class Control { UndoManager undoManager = new UndoManager(); public void undo() { undoManager.undo(); } } Reproduced on Context Found while turning bugs mined from real open-source Java (fixed upstream or still present) into study examples for the error-message study. ActivityMetadataMetadataAssigneesLabelsbugSomething isn't workingSomething isn't working TypeProjectsMilestoneRelationshipsDevelopmentIssue actions |
| You are visitor 01402503 — GeezerVison does not store the pages you look up. Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required. |