@@ -623,14 +623,14 @@ module CFG {
623
623
not cmpl .isNormal ( )
624
624
}
625
625
626
- predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
626
+ predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
627
627
exists ( int i |
628
628
lastNode ( this .getChildTreeRanked ( i ) , pred , normalCompletion ( ) ) and
629
629
firstNode ( this .getChildTreeRanked ( i + 1 ) , succ )
630
630
)
631
631
}
632
632
633
- predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) { this .succSimple ( pred , succ ) }
633
+ predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) { this .succ0 ( pred , succ ) }
634
634
635
635
final ControlFlowTree getChildTreeRanked ( int i ) {
636
636
exists ( int j |
@@ -729,8 +729,8 @@ module CFG {
729
729
last = this .getNode ( ) and cmpl = this .getCompletion ( )
730
730
}
731
731
732
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
733
- super .succSimple ( pred , succ )
732
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
733
+ super .succ0 ( pred , succ )
734
734
or
735
735
lastNode ( this .getLastChildTree ( ) , pred , normalCompletion ( ) ) and
736
736
succ = this .getNode ( )
@@ -752,8 +752,8 @@ module CFG {
752
752
cmpl = Done ( )
753
753
}
754
754
755
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
756
- super .succSimple ( pred , succ )
755
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
756
+ super .succ0 ( pred , succ )
757
757
or
758
758
pred = this .getNode ( ) and
759
759
firstNode ( this .getFirstChildTree ( ) , succ )
@@ -855,8 +855,8 @@ module CFG {
855
855
cmpl = Done ( )
856
856
}
857
857
858
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
859
- ControlFlowTree .super .succSimple ( pred , succ )
858
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
859
+ ControlFlowTree .super .succ0 ( pred , succ )
860
860
or
861
861
exists ( int i | lastNode ( this .getLhs ( i ) , pred , normalCompletion ( ) ) |
862
862
firstNode ( this .getLhs ( i + 1 ) , succ )
@@ -980,7 +980,7 @@ module CFG {
980
980
)
981
981
}
982
982
983
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
983
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
984
984
exists ( Completion lcmpl |
985
985
lastNode ( this .getLeftOperand ( ) , pred , lcmpl ) and
986
986
succ = this .getGuard ( lcmpl .getOutcome ( ) )
@@ -1030,11 +1030,11 @@ module CFG {
1030
1030
not result instanceof TypeExpr
1031
1031
}
1032
1032
1033
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1033
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1034
1034
// interpose implicit argument destructuring nodes between last argument
1035
1035
// and call itself; this is for cases like `f(g())` where `g` has multiple
1036
1036
// results
1037
- exists ( ControlFlow:: Node mid | PostOrderTree .super .succSimple ( pred , mid ) |
1037
+ exists ( ControlFlow:: Node mid | PostOrderTree .super .succ0 ( pred , mid ) |
1038
1038
if mid = this .getNode ( ) then succ = this .getEpilogueNode ( 0 ) else succ = mid
1039
1039
)
1040
1040
or
@@ -1104,8 +1104,8 @@ module CFG {
1104
1104
lastNode ( this .getStmt ( this .getNumStmt ( ) - 1 ) , last , cmpl )
1105
1105
}
1106
1106
1107
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1108
- ControlFlowTree .super .succSimple ( pred , succ )
1107
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1108
+ ControlFlowTree .super .succ0 ( pred , succ )
1109
1109
or
1110
1110
exists ( int i |
1111
1111
lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
@@ -1174,7 +1174,7 @@ module CFG {
1174
1174
cmpl = Done ( )
1175
1175
}
1176
1176
1177
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1177
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1178
1178
this .firstNode ( pred ) and
1179
1179
succ = this .getElementStart ( 0 )
1180
1180
or
@@ -1252,7 +1252,7 @@ module CFG {
1252
1252
cmpl = Done ( )
1253
1253
}
1254
1254
1255
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1255
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1256
1256
lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
1257
1257
firstNode ( this .getCond ( ) , succ )
1258
1258
or
@@ -1283,7 +1283,7 @@ module CFG {
1283
1283
( cmpl = Done ( ) or cmpl = Panic ( ) )
1284
1284
}
1285
1285
1286
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1286
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1287
1287
lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
1288
1288
(
1289
1289
succ = MkImplicitDeref ( this .getBase ( ) )
@@ -1320,8 +1320,8 @@ module CFG {
1320
1320
1321
1321
override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
1322
1322
1323
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1324
- ControlFlowTree .super .succSimple ( pred , succ )
1323
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1324
+ ControlFlowTree .super .succ0 ( pred , succ )
1325
1325
or
1326
1326
pred = MkEntryNode ( this ) and
1327
1327
firstNode ( this .getDecl ( 0 ) , succ )
@@ -1376,7 +1376,7 @@ module CFG {
1376
1376
i = 5 and result = this .getBody ( )
1377
1377
}
1378
1378
1379
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1379
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1380
1380
exists ( int i , ControlFlowTree predTree , Completion cmpl |
1381
1381
predTree = this .getChildTreeRanked ( i ) and
1382
1382
lastNode ( predTree , pred , cmpl ) and
@@ -1442,13 +1442,13 @@ module CFG {
1442
1442
// `defer` can be the first `defer` statement executed
1443
1443
// there is always a predecessor node because the `defer`'s call is always
1444
1444
// evaluated before the defer statement itself
1445
- MkDeferNode ( defer ) = succSimple ( notDeferSuccSimple * ( this .getEntry ( ) ) )
1445
+ MkDeferNode ( defer ) = succ0 ( notDefersucc0 * ( this .getEntry ( ) ) )
1446
1446
)
1447
1447
}
1448
1448
1449
1449
override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
1450
1450
1451
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1451
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1452
1452
exists ( int i |
1453
1453
pred = this .getPrologueNode ( i ) and
1454
1454
succ = this .getPrologueNode ( i + 1 )
@@ -1469,12 +1469,12 @@ module CFG {
1469
1469
}
1470
1470
1471
1471
override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1472
- this .succSimple ( pred , succ )
1472
+ this .succ0 ( pred , succ )
1473
1473
or
1474
1474
exists ( Completion cmpl |
1475
1475
lastNode ( this .getBody ( ) , pred , cmpl ) and
1476
1476
// last node of function body can be reached without going through a `defer` statement
1477
- pred = notDeferSuccSimple * ( this .getEntry ( ) )
1477
+ pred = notDefersucc0 * ( this .getEntry ( ) )
1478
1478
|
1479
1479
// panic goes directly to exit, non-panic reads result variables first
1480
1480
if cmpl = Panic ( ) then succ = MkExitNode ( this ) else succ = this .getEpilogueNode ( 0 )
@@ -1484,7 +1484,7 @@ module CFG {
1484
1484
exists ( DeferStmt defer | defer = this .getADeferStmt ( ) |
1485
1485
succ = MkExprNode ( defer .getCall ( ) ) and
1486
1486
// the last `DeferStmt` executed before pred is this `defer`
1487
- pred = notDeferSuccSimple * ( MkDeferNode ( defer ) )
1487
+ pred = notDefersucc0 * ( MkDeferNode ( defer ) )
1488
1488
)
1489
1489
or
1490
1490
exists ( DeferStmt predDefer , DeferStmt succDefer |
@@ -1522,7 +1522,7 @@ module CFG {
1522
1522
cmpl = Done ( )
1523
1523
}
1524
1524
1525
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1525
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1526
1526
lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
1527
1527
succ = MkImplicitOne ( this )
1528
1528
or
@@ -1553,7 +1553,7 @@ module CFG {
1553
1553
not cmpl .isNormal ( )
1554
1554
}
1555
1555
1556
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1556
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1557
1557
lastNode ( this .getDomain ( ) , pred , normalCompletion ( ) ) and
1558
1558
succ = MkNextNode ( this )
1559
1559
or
@@ -1628,7 +1628,7 @@ module CFG {
1628
1628
1629
1629
override Completion getCompletion ( ) { result = Return ( ) }
1630
1630
1631
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1631
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1632
1632
exists ( int i |
1633
1633
lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
1634
1634
succ = this .complete ( i )
@@ -1684,8 +1684,8 @@ module CFG {
1684
1684
)
1685
1685
}
1686
1686
1687
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1688
- ControlFlowTree .super .succSimple ( pred , succ )
1687
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1688
+ ControlFlowTree .super .succ0 ( pred , succ )
1689
1689
or
1690
1690
exists ( CommClause cc , int i , Stmt comm |
1691
1691
cc = this .getNonDefaultCommClause ( i ) and
@@ -1783,7 +1783,7 @@ module CFG {
1783
1783
cmpl = Done ( )
1784
1784
}
1785
1785
1786
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1786
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1787
1787
exists ( int i | pred = this .getStepWithRank ( i ) and succ = this .getStepWithRank ( i + 1 ) )
1788
1788
}
1789
1789
@@ -1820,8 +1820,8 @@ module CFG {
1820
1820
( cmpl = Done ( ) or cmpl = Panic ( ) )
1821
1821
}
1822
1822
1823
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1824
- ControlFlowTree .super .succSimple ( pred , succ )
1823
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1824
+ ControlFlowTree .super .succ0 ( pred , succ )
1825
1825
or
1826
1826
not this = any ( CommClause cc ) .getComm ( ) and
1827
1827
lastNode ( this .getValue ( ) , pred , normalCompletion ( ) ) and
@@ -1849,8 +1849,8 @@ module CFG {
1849
1849
( cmpl = Done ( ) or cmpl = Panic ( ) )
1850
1850
}
1851
1851
1852
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1853
- ControlFlowTree .super .succSimple ( pred , succ )
1852
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1853
+ ControlFlowTree .super .succ0 ( pred , succ )
1854
1854
or
1855
1855
lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
1856
1856
(
@@ -1936,8 +1936,8 @@ module CFG {
1936
1936
)
1937
1937
}
1938
1938
1939
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1940
- ControlFlowTree .super .succSimple ( pred , succ )
1939
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1940
+ ControlFlowTree .super .succ0 ( pred , succ )
1941
1941
or
1942
1942
lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
1943
1943
(
@@ -2010,8 +2010,8 @@ module CFG {
2010
2010
)
2011
2011
}
2012
2012
2013
- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
2014
- ControlFlowTree .super .succSimple ( pred , succ )
2013
+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
2014
+ ControlFlowTree .super .succ0 ( pred , succ )
2015
2015
or
2016
2016
not this = any ( RecvStmt recv ) .getExpr ( ) and
2017
2017
lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
@@ -2039,19 +2039,19 @@ module CFG {
2039
2039
}
2040
2040
2041
2041
/** Gets a successor of `nd` that is not a `defer` node */
2042
- private ControlFlow:: Node notDeferSuccSimple ( ControlFlow:: Node nd ) {
2042
+ private ControlFlow:: Node notDefersucc0 ( ControlFlow:: Node nd ) {
2043
2043
not result = MkDeferNode ( _) and
2044
- result = succSimple ( nd )
2044
+ result = succ0 ( nd )
2045
2045
}
2046
2046
2047
2047
/** Gets `defer` statements that can be the first defer statement after `nd` in the CFG */
2048
2048
private ControlFlow:: Node nextDefer ( ControlFlow:: Node nd ) {
2049
2049
nd = MkDeferNode ( _) and
2050
2050
result = MkDeferNode ( _) and
2051
2051
(
2052
- result = succSimple ( nd )
2052
+ result = succ0 ( nd )
2053
2053
or
2054
- result = succSimple ( notDeferSuccSimple + ( nd ) )
2054
+ result = succ0 ( notDefersucc0 + ( nd ) )
2055
2055
)
2056
2056
}
2057
2057
@@ -2082,9 +2082,7 @@ module CFG {
2082
2082
2083
2083
/** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
2084
2084
cached
2085
- ControlFlow:: Node succSimple ( ControlFlow:: Node nd ) {
2086
- any ( ControlFlowTree tree ) .succSimple ( nd , result )
2087
- }
2085
+ ControlFlow:: Node succ0 ( ControlFlow:: Node nd ) { any ( ControlFlowTree tree ) .succ0 ( nd , result ) }
2088
2086
2089
2087
/** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
2090
2088
cached
0 commit comments