@@ -71,6 +71,12 @@ signature module AstSig<LocationSig Location> {
7171 /** A statement. */
7272 class Stmt extends AstNode ;
7373
74+ /** A labeled statement. */
75+ class LabeledStmt extends Stmt {
76+ /** Gets the statement carrying the label. */
77+ Stmt getStmt ( ) ;
78+ }
79+
7480 /** An expression. */
7581 class Expr extends AstNode ;
7682
@@ -439,10 +445,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
439445 string toString ( ) ;
440446 }
441447
442- /**
443- * Holds if the node `n` has the label `l`. For example, a label in a goto
444- * statement or a goto target.
445- */
448+ /** Holds if the node `n` directly has the label `l`. */
446449 default predicate hasLabel ( AstNode n , Label l ) { none ( ) }
447450
448451 /**
@@ -1282,9 +1285,23 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
12821285 )
12831286 }
12841287
1285- private Stmt getAStmtInBlock ( AstNode block ) {
1286- result = block .( BlockStmt ) .getStmt ( _) or
1287- result = block .( Switch ) .getStmt ( _)
1288+ /** Holds if `n` has `l`, possibly through enclosing labeled statements. */
1289+ private predicate hasLabel ( AstNode n , Input1:: Label l ) {
1290+ Input1:: hasLabel ( n , l )
1291+ or
1292+ exists ( LabeledStmt labeled | labeled .getStmt ( ) = n and hasLabel ( labeled , l ) )
1293+ }
1294+
1295+ /**
1296+ * Holds if `target` is a labeled statement at the start of `root`,
1297+ * possibly nested under other labeled statements.
1298+ */
1299+ private predicate labeledTargetInRoot ( Stmt root , LabeledStmt target ) {
1300+ root = target
1301+ or
1302+ exists ( LabeledStmt labeled |
1303+ root = labeled and labeledTargetInRoot ( labeled .getStmt ( ) , target )
1304+ )
12881305 }
12891306
12901307 private predicate callableHasParamDefault ( Callable c , Expr defaultValue ) {
@@ -1325,7 +1342,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
13251342 or
13261343 exists ( Input1:: Label l |
13271344 c .hasLabel ( l ) and
1328- Input1 :: hasLabel ( loop , l )
1345+ hasLabel ( loop , l )
13291346 )
13301347 )
13311348 )
@@ -1365,16 +1382,32 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
13651382 or
13661383 exists ( Input1:: Label l |
13671384 c .hasLabel ( l ) and
1368- Input1 :: hasLabel ( switch , l )
1385+ hasLabel ( switch , l )
13691386 )
13701387 )
13711388 or
1372- exists ( AstNode block , Input1:: Label l , Stmt lblstmt |
1373- ast = getAStmtInBlock ( block ) and
1374- lblstmt = getAStmtInBlock ( block ) and
1375- not lblstmt instanceof GotoStmt and
1376- Input1:: hasLabel ( pragma [ only_bind_into ] ( lblstmt ) , l ) and
1377- n .isBefore ( lblstmt ) and
1389+ exists ( LabeledStmt target , Input1:: Label l |
1390+ ast = target .getStmt ( ) and
1391+ Input1:: hasLabel ( target , l ) and
1392+ n .isAfter ( target ) and
1393+ c .getSuccessorType ( ) instanceof BreakSuccessor and
1394+ c .hasLabel ( l )
1395+ )
1396+ or
1397+ exists ( AstNode parent , Stmt root , LabeledStmt target , Input1:: Label l |
1398+ ast = getChild ( parent , _) and
1399+ root = getChild ( parent , _) and
1400+ labeledTargetInRoot ( root , target ) and
1401+ Input1:: hasLabel ( target , l ) and
1402+ n .isBefore ( target ) and
1403+ c .getSuccessorType ( ) instanceof GotoSuccessor and
1404+ c .hasLabel ( l )
1405+ )
1406+ or
1407+ exists ( LabeledStmt target , Input1:: Label l |
1408+ ast = target .getStmt ( ) and
1409+ Input1:: hasLabel ( target , l ) and
1410+ n .isBefore ( target ) and
13781411 c .getSuccessorType ( ) instanceof GotoSuccessor and
13791412 c .hasLabel ( l )
13801413 )
0 commit comments