@@ -1136,6 +1136,22 @@ private predicate inForUpdate(Expr forUpdate, Expr child) {
1136
1136
exists ( Expr mid | inForUpdate ( forUpdate , mid ) and child .getParent ( ) = mid )
1137
1137
}
1138
1138
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
+
1139
1155
/**
1140
1156
* A C/C++ 'switch case' statement.
1141
1157
*
@@ -1331,16 +1347,19 @@ class SwitchCase extends Stmt, @stmt_switch_case {
1331
1347
* `default:` has results `{ x = 3; }, `x = 4;` and `break;`.
1332
1348
*/
1333
1349
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 ) )
1343
1358
)
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 ) )
1344
1363
)
1345
1364
}
1346
1365
0 commit comments