@@ -780,7 +780,7 @@ module ControlFlow {
780780 TLastRecNonContinueCompletion ( ) or
781781 TLastRecLoopBodyAbnormal ( )
782782
783- private TLastComputation selfValid ( ControlFlowElement cfe ) {
783+ private TSelf getValidSelfCompletion ( ControlFlowElement cfe ) {
784784 result = TSelf ( any ( Completion c | c .isValidFor ( cfe ) ) )
785785 }
786786
@@ -801,13 +801,13 @@ module ControlFlow {
801801 or
802802 ss .isLeafElement ( ) and
803803 result = ss and
804- c = selfValid ( result )
804+ c = getValidSelfCompletion ( result )
805805 )
806806 or
807807 // Post-order: element itself
808808 cfe instanceof StandardExpr and
809809 result = cfe and
810- c = selfValid ( result )
810+ c = getValidSelfCompletion ( result )
811811 or
812812 // Pre/post order: a child exits abnormally
813813 result = cfe .( StandardElement ) .getChildElement ( _) and
@@ -883,7 +883,7 @@ module ControlFlow {
883883 cfe = any ( ConditionallyQualifiedExpr cqe |
884884 // Post-order: element itself
885885 result = cqe and
886- c = selfValid ( result )
886+ c = getValidSelfCompletion ( result )
887887 or
888888 // Qualifier exits with a `null` completion
889889 result = cqe .getChildExpr ( - 1 ) and
@@ -893,7 +893,7 @@ module ControlFlow {
893893 cfe = any ( ThrowExpr te |
894894 // Post-order: element itself
895895 result = te and
896- c = selfValid ( result )
896+ c = getValidSelfCompletion ( result )
897897 or
898898 // Expression being thrown exits abnormally
899899 result = te .getExpr ( ) and
@@ -904,7 +904,7 @@ module ControlFlow {
904904 // Post-order: element itself (when no initializer)
905905 result = oc and
906906 not oc .hasInitializer ( ) and
907- c = selfValid ( result )
907+ c = getValidSelfCompletion ( result )
908908 or
909909 // Last element of initializer
910910 result = oc .getInitializer ( ) and
@@ -915,7 +915,7 @@ module ControlFlow {
915915 // Post-order: element itself (when no initializer)
916916 result = ac and
917917 not ac .hasInitializer ( ) and
918- c = selfValid ( result )
918+ c = getValidSelfCompletion ( result )
919919 or
920920 // Last element of initializer
921921 result = ac .getInitializer ( ) and
@@ -1091,7 +1091,7 @@ module ControlFlow {
10911091 cfe = any ( JumpStmt js |
10921092 // Post-order: element itself
10931093 result = js and
1094- c = selfValid ( result )
1094+ c = getValidSelfCompletion ( result )
10951095 or
10961096 // Child exits abnormally
10971097 result = js .getChild ( 0 ) and
@@ -1111,7 +1111,7 @@ module ControlFlow {
11111111 cfe = any ( AccessorWrite aw |
11121112 // Post-order: element itself
11131113 result = aw and
1114- c = selfValid ( result )
1114+ c = getValidSelfCompletion ( result )
11151115 or
11161116 // A child exits abnormally
11171117 result = getExprChildElement ( aw , _) and
@@ -1233,6 +1233,11 @@ module ControlFlow {
12331233 )
12341234 }
12351235
1236+ /**
1237+ * Gets a potential last element executed within control flow element `cfe`,
1238+ * as well as its completion, where the last element of `cfe` is recursively
1239+ * computed as specified by `rec`.
1240+ */
12361241 pragma [ nomagic]
12371242 private ControlFlowElement lastRec (
12381243 ControlFlowElement cfe , Completion c , TLastRecComputation rec
@@ -1244,10 +1249,7 @@ module ControlFlow {
12441249 private ControlFlowElement lastRecSpecific (
12451250 ControlFlowElement cfe , Completion c1 , Completion c2
12461251 ) {
1247- exists ( TLastRecComputation rec |
1248- result = lastRec ( cfe , c1 , rec ) and
1249- rec = TLastRecSpecificCompletion ( c2 )
1250- )
1252+ result = lastRec ( cfe , c1 , TLastRecSpecificCompletion ( c2 ) )
12511253 }
12521254
12531255 pragma [ nomagic]
0 commit comments