[CatarinaGamboa]

Fixes #494

The verifier had no switch handling, so the cases ran one after another as straight-line code: break was ignored and the case label never entered the path condition. A switch is now checked like the if / else if chain over its labels:

• each case starts from the state before the switch and knows selector == label (grouped labels: any of them; default: none of the other labels)
• a case without break falls through into the next one
• the states of the cases that reach the end are joined after the switch, as after an if
• return / throw / continue in a case drop that path, as in an if
• switch expressions (->, yield) are checked the same way; selectors may be enums, ints or strings (a string label has no known value, so it adds no path condition)

Two forms are handled conservatively:

• pattern or guarded cases (case String s ->, when): checked as before (Verifier crashes on a type-pattern switch (case String s ->) #345 is unchanged)
• a break / yield nested inside a case (e.g. if (c) { ...; break; }): the state at that jump is not followed, so what those cases change is forgotten on that path after the switch (shown as true in Found)

Study exercise A1_09 (litiengine), the partial fix else if (newMode == BORDERLESS) host.dispose();

Before, the same error at the same line, though BORDERLESS is now disposed:

State Refinement Error: found previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host) : (newMode == BORDERLESS ? notDisplayable(host) : displayable(host)) but expected notDisplayable(host)
49 |         host.setUndecorated(true);

After, the error moves to the remaining bug, the full-screen fallback:

State Refinement Error: found newMode == FULLSCREEN && (previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host) : (newMode == BORDERLESS ? notDisplayable(host) : displayable(host))) but expected notDisplayable(host)
62 |           host.setUndecorated(true);

Study exercise A1_56 (JabRef), only redo() guarded

Before, the UNDO case saw what the REDO case did:

State Refinement Error: found (#canRedo_result ? redoable(undoManager@70) : notRedoable(undoManager@70)) && state2(undoManager@70) == state2(#getUndoManager_result) && limit(undoManager@70) == limit(#getUndoManager_result) && (#canRedo_result ? undoable(undoManager) && notRedoable(undoManager) && ... : ...) but expected undoable(undoManager)

After, only what holds on the UNDO path:

State Refinement Error: expected undoable(undoManager) but could not prove it
72 |                     case UNDO -> undoManager.undo();
Hints:
  - The state of undoManager is unknown here, and this call needs it to be undoable
  - Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable

The six study exercises still report their error at the same line. A1_09's Found now starts with the case's label: found newMode == BORDERLESS && (...). The other study variants report the same as before, apart from A1_09's first-only fix: same line (63), but its Found was displayable(host), the state the BORDERLESS case left, and is now the full-screen path's newMode == FULLSCREEN && (...), longer than before.

Tests: CorrectEnumUsage (state and label of each case, switch statement and expression), ErrorEnumUsage (an error that was missed in a case reached directly and by fall-through, and the nested break). TestStateHints now expects A1_56's UNDO hints above. Each fails on main.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

[P2] Exclude the unmatched path for exhaustive enum switches (RefinementTypeChecker.java:671-672). When a switch covers every constant of an enum but has no default, this branch still treats "no label matches" as a path that reaches the code after the switch. For example, if every case moves an object to the same required typestate, the join also includes its pre-switch state and can incorrectly reject a valid call afterward. Detect exhaustive enum switches before adding the unmatched path.

[CatarinaGamboa]

Round 1 replies:

• Exhaustive enum switches: partly fixed, partly declined.
  • Declined for enums declared in the analyzed sources. Their constants are values of an SMT enum sort, so when every constant has a case, "no label matches" is already unsatisfiable. I checked: a switch statement with case RED / GREEN / BLUE that each close(), followed by reopen(), verifies.
  • Declined for switch statements over library enums. A switch statement with no default really can match no label: Java adds no default, so a constant added to the enum later reaches the code after it.
  • Fixed for switch expressions, which Java makes exhaustive: when no label matches, the code it adds throws. That path no longer reaches the code after the switch. Covered by CorrectEnumUsage.captureOnThread, on Thread.State, a library enum whose labels the verifier cannot translate. That test fails without the change.

[CatarinaGamboa]

Codex review, round 2: no findings ("I found no actionable regressions in the diff. The verifier test suite passed.").