| Issue 17: | Unpacking does not purify invariants above root node | |
| 1 person starred this issue and may be notified of changes. | Back to list |
Invariants above the unpacked root node are not purified. |
| Issue 17: | Unpacking does not purify invariants above root node | |
| 1 person starred this issue and may be notified of changes. | Back to list |
Invariants above the unpacked root node are not purified. |
Kevin's last email said that he thought this was finished but the following code I think should have a warning: @States({"S1","S2"}) @ClassStates(@State(name="alive", inv="full(myField)")) @NonReentrant public class Issue17Test { private Object myField; @Full(guarantee="S1", use=Use.FIELDS) void canICallPure() { needsPure(myField); } private static void needsPure(@Pure Object obj) {} @Full(guarantee="S1", use=Use.FIELDS) void canICallFull() { needsFull(myField); // Warning here, right? } private static void needsFull(@Full Object obj) {} }