Skip to content

Commit 8e5ff7b

Browse files
paldepindCopilot
andcommitted
Use shared exhaustive-switch handling for Java
Declare exhaustive Java switch constructs through isExhaustive while retaining language-specific default and Object-pattern match-all cases. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4a9b52f8-d07b-4692-8fb9-409f0efd64f2
1 parent 259e0b4 commit 8e5ff7b

1 file changed

Lines changed: 10 additions & 13 deletions

File tree

‎java/ql/lib/semmle/code/java/ControlFlowGraph.qll‎

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -513,23 +513,20 @@ private module Input implements InputSig1, InputSig2 {
513513
)
514514
}
515515

516+
/** Holds if this switch must be exhaustive. */
517+
predicate isExhaustive(Ast::Switch switch) {
518+
// Switch expressions and enhanced switch blocks (those that use pattern
519+
// cases or match null) must be exhaustive.
520+
// See https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2
521+
switch instanceof SwitchExpr or
522+
exists(switch.(SwitchStmt).getAPatternCase()) or
523+
switch.(SwitchStmt).hasNullCase()
524+
}
525+
516526
/** Holds if this case matches all possible values. */
517527
predicate matchAll(Ast::Case c) {
518528
c instanceof DefaultCase
519529
or
520-
// Switch expressions and enhanced switch blocks (those that use pattern
521-
// cases or match null) must be exhaustive, so the last case matches all
522-
// remaining values.
523-
// See https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2
524-
exists(Ast::Switch switch, int last |
525-
switch instanceof SwitchExpr or
526-
exists(switch.(SwitchStmt).getAPatternCase()) or
527-
switch.(SwitchStmt).hasNullCase()
528-
|
529-
switch.getCase(last) = c and
530-
not exists(switch.getCase(last + 1))
531-
)
532-
or
533530
c.(J::PatternCase).getAPattern().getType() instanceof TypeObject
534531
}
535532

0 commit comments

Comments
 (0)