@@ -224,6 +224,17 @@ signature module AstSig<LocationSig Location> {
224224
225225 /** Gets the case at the specified (zero-based) `index`. */
226226 Case getCase ( int index ) ;
227+
228+ /**
229+ * Gets the statement at the specified (zero-based) `index`, if any.
230+ *
231+ * Depending on the language, switches may have their case bodies nested
232+ * under the case nodes, which may or may not be statements themselves, or
233+ * the switches may have a flat structure where the cases are just labels
234+ * and the case bodies are sequences of statements between case statements.
235+ * This predicate accomodates the latter.
236+ */
237+ Stmt getStmt ( int index ) ;
227238 }
228239
229240 /** A case in a switch. */
@@ -235,12 +246,13 @@ signature module AstSig<LocationSig Location> {
235246 Expr getGuard ( ) ;
236247
237248 /**
238- * Gets the body element of this case at the specified (zero-based) `index` .
249+ * Gets the body of this case, if any .
239250 *
240- * This is either unique when the case has a single right-hand side, or it
241- * is the sequence of statements between this case and the next case.
251+ * A case can either have a body as a single child AST node given by this
252+ * predicate, or it can have an implicit body given by the sequence of
253+ * statements between this case and the next case.
242254 */
243- AstNode getBodyElement ( int index ) ;
255+ AstNode getBody ( ) ;
244256 }
245257
246258 class DefaultCase extends Case ;
@@ -1075,7 +1087,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
10751087 )
10761088 or
10771089 exists ( Switch switch |
1078- ast = switch .getCase ( _) . getBodyElement ( _) and
1090+ ast = getCaseBodyElement ( switch .getCase ( _) , _) and
10791091 n .isAfter ( switch ) and
10801092 c .getSuccessorType ( ) instanceof BreakSuccessor
10811093 |
@@ -1107,10 +1119,40 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
11071119 result = rank [ rnk ] ( Case c , int i | getCaseControlFlowOrder ( s , c ) = i | c order by i )
11081120 }
11091121
1122+ private int numberOfStmts ( Switch s ) { result = strictcount ( s .getStmt ( _) ) }
1123+
1124+ private predicate caseIndex ( Switch s , Case c , int caseIdx , int caseStmtPos ) {
1125+ c = s .getCase ( caseIdx ) and
1126+ c = s .getStmt ( caseStmtPos )
1127+ }
1128+
1129+ /**
1130+ * Gets the body element of `case` at the specified (zero-based) `index`.
1131+ *
1132+ * This is either unique when the case has a single right-hand side, or it
1133+ * is the sequence of statements between this case and the next case.
1134+ */
1135+ private AstNode getCaseBodyElement ( Case case , int index ) {
1136+ result = case .getBody ( ) and index = 0
1137+ or
1138+ not exists ( case .getBody ( ) ) and
1139+ exists ( Switch s , int caseIdx , int caseStmtPos , int nextCaseStmtPos |
1140+ caseIndex ( pragma [ only_bind_into ] ( s ) , case , caseIdx , caseStmtPos ) and
1141+ (
1142+ caseIndex ( pragma [ only_bind_into ] ( s ) , _, caseIdx + 1 , nextCaseStmtPos )
1143+ or
1144+ not exists ( s .getCase ( caseIdx + 1 ) ) and
1145+ nextCaseStmtPos = numberOfStmts ( s )
1146+ ) and
1147+ index = [ 0 .. nextCaseStmtPos - caseStmtPos - 2 ] and
1148+ result = pragma [ only_bind_into ] ( s ) .getStmt ( caseStmtPos + 1 + index )
1149+ )
1150+ }
1151+
11101152 private AstNode getFirstCaseBodyElement ( Case case ) {
1111- result = case . getBodyElement ( 0 )
1153+ result = getCaseBodyElement ( case , 0 )
11121154 or
1113- not exists ( case . getBodyElement ( 0 ) ) and
1155+ not exists ( getCaseBodyElement ( case , 0 ) ) and
11141156 exists ( Switch s , int i |
11151157 fallsThrough ( case ) and
11161158 // fall-through follows AST order, not case control flow order:
@@ -1120,10 +1162,10 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
11201162 }
11211163
11221164 private AstNode getNextCaseBodyElement ( AstNode bodyElement ) {
1123- exists ( Case case , int i | case . getBodyElement ( i ) = bodyElement |
1124- result = case . getBodyElement ( i + 1 )
1165+ exists ( Case case , int i | getCaseBodyElement ( case , i ) = bodyElement |
1166+ result = getCaseBodyElement ( case , i + 1 )
11251167 or
1126- not exists ( case . getBodyElement ( i + 1 ) ) and
1168+ not exists ( getCaseBodyElement ( case , i + 1 ) ) and
11271169 exists ( Switch s , int j |
11281170 fallsThrough ( case ) and
11291171 // fall-through follows AST order, not case control flow order:
@@ -1474,7 +1516,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
14741516 or
14751517 n1 .isAfter ( caseBodyElement ) and
14761518 not exists ( getNextCaseBodyElement ( caseBodyElement ) ) and
1477- n2 .isAfter ( any ( Switch s | s .getCase ( _) . getBodyElement ( _) = caseBodyElement ) )
1519+ n2 .isAfter ( any ( Switch s | getCaseBodyElement ( s .getCase ( _) , _) = caseBodyElement ) )
14781520 )
14791521 }
14801522
0 commit comments