@@ -623,14 +623,14 @@ module CFG {
623623 not cmpl .isNormal ( )
624624 }
625625
626- predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
626+ predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
627627 exists ( int i |
628628 lastNode ( this .getChildTreeRanked ( i ) , pred , normalCompletion ( ) ) and
629629 firstNode ( this .getChildTreeRanked ( i + 1 ) , succ )
630630 )
631631 }
632632
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 ) }
634634
635635 final ControlFlowTree getChildTreeRanked ( int i ) {
636636 exists ( int j |
@@ -729,8 +729,8 @@ module CFG {
729729 last = this .getNode ( ) and cmpl = this .getCompletion ( )
730730 }
731731
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 )
734734 or
735735 lastNode ( this .getLastChildTree ( ) , pred , normalCompletion ( ) ) and
736736 succ = this .getNode ( )
@@ -752,8 +752,8 @@ module CFG {
752752 cmpl = Done ( )
753753 }
754754
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 )
757757 or
758758 pred = this .getNode ( ) and
759759 firstNode ( this .getFirstChildTree ( ) , succ )
@@ -855,8 +855,8 @@ module CFG {
855855 cmpl = Done ( )
856856 }
857857
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 )
860860 or
861861 exists ( int i | lastNode ( this .getLhs ( i ) , pred , normalCompletion ( ) ) |
862862 firstNode ( this .getLhs ( i + 1 ) , succ )
@@ -980,7 +980,7 @@ module CFG {
980980 )
981981 }
982982
983- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
983+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
984984 exists ( Completion lcmpl |
985985 lastNode ( this .getLeftOperand ( ) , pred , lcmpl ) and
986986 succ = this .getGuard ( lcmpl .getOutcome ( ) )
@@ -1030,11 +1030,11 @@ module CFG {
10301030 not result instanceof TypeExpr
10311031 }
10321032
1033- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1033+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
10341034 // interpose implicit argument destructuring nodes between last argument
10351035 // and call itself; this is for cases like `f(g())` where `g` has multiple
10361036 // results
1037- exists ( ControlFlow:: Node mid | PostOrderTree .super .succSimple ( pred , mid ) |
1037+ exists ( ControlFlow:: Node mid | PostOrderTree .super .succ0 ( pred , mid ) |
10381038 if mid = this .getNode ( ) then succ = this .getEpilogueNode ( 0 ) else succ = mid
10391039 )
10401040 or
@@ -1104,8 +1104,8 @@ module CFG {
11041104 lastNode ( this .getStmt ( this .getNumStmt ( ) - 1 ) , last , cmpl )
11051105 }
11061106
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 )
11091109 or
11101110 exists ( int i |
11111111 lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
@@ -1174,7 +1174,7 @@ module CFG {
11741174 cmpl = Done ( )
11751175 }
11761176
1177- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1177+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
11781178 this .firstNode ( pred ) and
11791179 succ = this .getElementStart ( 0 )
11801180 or
@@ -1252,7 +1252,7 @@ module CFG {
12521252 cmpl = Done ( )
12531253 }
12541254
1255- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1255+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
12561256 lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
12571257 firstNode ( this .getCond ( ) , succ )
12581258 or
@@ -1283,7 +1283,7 @@ module CFG {
12831283 ( cmpl = Done ( ) or cmpl = Panic ( ) )
12841284 }
12851285
1286- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1286+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
12871287 lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
12881288 (
12891289 succ = MkImplicitDeref ( this .getBase ( ) )
@@ -1320,8 +1320,8 @@ module CFG {
13201320
13211321 override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
13221322
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 )
13251325 or
13261326 pred = MkEntryNode ( this ) and
13271327 firstNode ( this .getDecl ( 0 ) , succ )
@@ -1376,7 +1376,7 @@ module CFG {
13761376 i = 5 and result = this .getBody ( )
13771377 }
13781378
1379- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1379+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
13801380 exists ( int i , ControlFlowTree predTree , Completion cmpl |
13811381 predTree = this .getChildTreeRanked ( i ) and
13821382 lastNode ( predTree , pred , cmpl ) and
@@ -1442,13 +1442,13 @@ module CFG {
14421442 // `defer` can be the first `defer` statement executed
14431443 // there is always a predecessor node because the `defer`'s call is always
14441444 // evaluated before the defer statement itself
1445- MkDeferNode ( defer ) = succSimple ( notDeferSuccSimple * ( this .getEntry ( ) ) )
1445+ MkDeferNode ( defer ) = succ0 ( notDefersucc0 * ( this .getEntry ( ) ) )
14461446 )
14471447 }
14481448
14491449 override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
14501450
1451- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1451+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
14521452 exists ( int i |
14531453 pred = this .getPrologueNode ( i ) and
14541454 succ = this .getPrologueNode ( i + 1 )
@@ -1469,12 +1469,12 @@ module CFG {
14691469 }
14701470
14711471 override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1472- this .succSimple ( pred , succ )
1472+ this .succ0 ( pred , succ )
14731473 or
14741474 exists ( Completion cmpl |
14751475 lastNode ( this .getBody ( ) , pred , cmpl ) and
14761476 // last node of function body can be reached without going through a `defer` statement
1477- pred = notDeferSuccSimple * ( this .getEntry ( ) )
1477+ pred = notDefersucc0 * ( this .getEntry ( ) )
14781478 |
14791479 // panic goes directly to exit, non-panic reads result variables first
14801480 if cmpl = Panic ( ) then succ = MkExitNode ( this ) else succ = this .getEpilogueNode ( 0 )
@@ -1484,7 +1484,7 @@ module CFG {
14841484 exists ( DeferStmt defer | defer = this .getADeferStmt ( ) |
14851485 succ = MkExprNode ( defer .getCall ( ) ) and
14861486 // the last `DeferStmt` executed before pred is this `defer`
1487- pred = notDeferSuccSimple * ( MkDeferNode ( defer ) )
1487+ pred = notDefersucc0 * ( MkDeferNode ( defer ) )
14881488 )
14891489 or
14901490 exists ( DeferStmt predDefer , DeferStmt succDefer |
@@ -1522,7 +1522,7 @@ module CFG {
15221522 cmpl = Done ( )
15231523 }
15241524
1525- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1525+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
15261526 lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
15271527 succ = MkImplicitOne ( this )
15281528 or
@@ -1553,7 +1553,7 @@ module CFG {
15531553 not cmpl .isNormal ( )
15541554 }
15551555
1556- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1556+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
15571557 lastNode ( this .getDomain ( ) , pred , normalCompletion ( ) ) and
15581558 succ = MkNextNode ( this )
15591559 or
@@ -1628,7 +1628,7 @@ module CFG {
16281628
16291629 override Completion getCompletion ( ) { result = Return ( ) }
16301630
1631- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1631+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
16321632 exists ( int i |
16331633 lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
16341634 succ = this .complete ( i )
@@ -1684,8 +1684,8 @@ module CFG {
16841684 )
16851685 }
16861686
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 )
16891689 or
16901690 exists ( CommClause cc , int i , Stmt comm |
16911691 cc = this .getNonDefaultCommClause ( i ) and
@@ -1783,7 +1783,7 @@ module CFG {
17831783 cmpl = Done ( )
17841784 }
17851785
1786- override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1786+ override predicate succ0 ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
17871787 exists ( int i | pred = this .getStepWithRank ( i ) and succ = this .getStepWithRank ( i + 1 ) )
17881788 }
17891789
@@ -1820,8 +1820,8 @@ module CFG {
18201820 ( cmpl = Done ( ) or cmpl = Panic ( ) )
18211821 }
18221822
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 )
18251825 or
18261826 not this = any ( CommClause cc ) .getComm ( ) and
18271827 lastNode ( this .getValue ( ) , pred , normalCompletion ( ) ) and
@@ -1849,8 +1849,8 @@ module CFG {
18491849 ( cmpl = Done ( ) or cmpl = Panic ( ) )
18501850 }
18511851
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 )
18541854 or
18551855 lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
18561856 (
@@ -1936,8 +1936,8 @@ module CFG {
19361936 )
19371937 }
19381938
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 )
19411941 or
19421942 lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
19431943 (
@@ -2010,8 +2010,8 @@ module CFG {
20102010 )
20112011 }
20122012
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 )
20152015 or
20162016 not this = any ( RecvStmt recv ) .getExpr ( ) and
20172017 lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
@@ -2039,19 +2039,19 @@ module CFG {
20392039 }
20402040
20412041 /** 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 ) {
20432043 not result = MkDeferNode ( _) and
2044- result = succSimple ( nd )
2044+ result = succ0 ( nd )
20452045 }
20462046
20472047 /** Gets `defer` statements that can be the first defer statement after `nd` in the CFG */
20482048 private ControlFlow:: Node nextDefer ( ControlFlow:: Node nd ) {
20492049 nd = MkDeferNode ( _) and
20502050 result = MkDeferNode ( _) and
20512051 (
2052- result = succSimple ( nd )
2052+ result = succ0 ( nd )
20532053 or
2054- result = succSimple ( notDeferSuccSimple + ( nd ) )
2054+ result = succ0 ( notDefersucc0 + ( nd ) )
20552055 )
20562056 }
20572057
@@ -2082,9 +2082,7 @@ module CFG {
20822082
20832083 /** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
20842084 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 ) }
20882086
20892087 /** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
20902088 cached
0 commit comments