Repository navigation
False error: a break nested inside a switch case forgets that path's state (Found shows true) #499
Description
Follow-up to #494 / #497. With switch cases modelled, a break nested inside a case (for example inside an if) is not followed: the state at that break is dropped, so after the switch the verifier knows nothing about that path. Correct code is rejected, and the message shows a bare true.
@StateSet({"closed", "open"})
class Door {
@StateRefinement(to = "closed(this)") Door() {}
@StateRefinement(from = "closed(this)", to = "open(this)") void open() {}
@StateRefinement(from = "open(this)", to = "closed(this)") void close() {}
}
class NestedBreak {
// Every path opens the door before leaving the switch, so close() is fine
static void enter(int k, boolean fast) {
Door d = new Door();
switch (k) {
case 1:
if (fast) {
d.open();
break;
}
d.open();
break;
default:
d.open();
}
d.close();
}
}State Refinement Error: found k == 1 ? true : open(d) but expected open(d)
31 | d.close();
Hints:
- d can be in closed or open here, depending on the path taken, and no sequence of calls moves all of them to open. Make d reach this line in the same state on every path
Expected: no error. The true means "forgotten", which users are not told, and the hint describes a split that does not exist.
Fix direction: record the context at each nested break / yield and join it with the cases' end states, as loops already do for their exits.
Not needed for the error-message study (no study exercise has this shape after a switch).
Activity