@@ -1136,20 +1136,9 @@ 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
- )
1139
+ /** Gets the `rnk`'th `case` statement in `b`. */
1140
+ private int indexOfSwitchCaseRank ( BlockStmt b , int rnk ) {
1141
+ result = rank [ rnk ] ( int i | b .getStmt ( i ) instanceof SwitchCase )
1153
1142
}
1154
1143
1155
1144
/**
@@ -1347,19 +1336,14 @@ class SwitchCase extends Stmt, @stmt_switch_case {
1347
1336
* `default:` has results `{ x = 3; }, `x = 4;` and `break;`.
1348
1337
*/
1349
1338
Stmt getAStmt ( ) {
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 ) )
1358
- )
1339
+ exists ( BlockStmt b , int rnk , int i |
1340
+ b .getStmt ( i ) = this and
1341
+ i = indexOfSwitchCaseRank ( b , rnk )
1342
+ |
1343
+ pragma [ only_bind_into ] ( b ) .getStmt ( [ i + 1 .. indexOfSwitchCaseRank ( b , rnk + 1 ) - 1 ] ) = result
1359
1344
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 ) )
1345
+ not exists ( indexOfSwitchCaseRank ( b , rnk + 1 ) ) and
1346
+ b .getStmt ( [ i + 1 .. b .getNumStmt ( ) + 1 ] ) = result
1363
1347
)
1364
1348
}
1365
1349
0 commit comments