@@ -1136,6 +1136,22 @@ private predicate inForUpdate(Expr forUpdate, Expr child) {
11361136 exists ( Expr mid | inForUpdate ( forUpdate , mid ) and child .getParent ( ) = mid )
11371137}
11381138
1139+ /**
1140+ * Holds if `next` is the first `SwitchCase` after `case` that is enclosed by the `BlockStmt` `b`.
1141+ */
1142+ pragma [ nomagic]
1143+ private predicate nextSwitchCaseInSameBlock ( BlockStmt b , SwitchCase case , SwitchCase next ) {
1144+ // If the next switch case is in the block `b` we're done.
1145+ case .getNextSwitchCase ( ) = next and
1146+ next .getEnclosingBlock ( ) = b
1147+ or
1148+ // Otherwise, skip past the next switch block when it's not enclosed in the block `b`.
1149+ exists ( SwitchCase mid | mid = case .getNextSwitchCase ( ) |
1150+ not mid .getEnclosingBlock ( ) = b and
1151+ nextSwitchCaseInSameBlock ( b , mid , next )
1152+ )
1153+ }
1154+
11391155/**
11401156 * A C/C++ 'switch case' statement.
11411157 *
@@ -1331,16 +1347,19 @@ class SwitchCase extends Stmt, @stmt_switch_case {
13311347 * `default:` has results `{ x = 3; }, `x = 4;` and `break;`.
13321348 */
13331349 Stmt getAStmt ( ) {
1334- exists ( BlockStmt b , int i , int j |
1335- b .getStmt ( i ) = this and
1336- b .getStmt ( j ) = result and
1337- i < j and
1338- not result instanceof SwitchCase and
1339- not exists ( SwitchCase sc , int k |
1340- b .getStmt ( k ) = sc and
1341- i < k and
1342- j > k
1350+ exists ( BlockStmt b , int i | this = b .getStmt ( i ) |
1351+ // This is the most usual case:
1352+ // We locate the next `SwitchCase` and pick a statement between this `SwitchCase` and the `SwitchCase`
1353+ // in the `j`'th position in the block `b`.
1354+ exists ( int j |
1355+ nextSwitchCaseInSameBlock ( b , this ,
1356+ pragma [ only_bind_into ] ( b ) .getStmt ( pragma [ only_bind_into ] ( j ) ) ) and
1357+ result = b .getStmt ( any ( int k | i < k and k < j ) )
13431358 )
1359+ or
1360+ // If there is no next switch case we pick any subsequent statement in the block `b`.
1361+ not nextSwitchCaseInSameBlock ( b , this , _) and
1362+ result = b .getStmt ( any ( int k | i < k ) )
13441363 )
13451364 }
13461365
0 commit comments