@@ -746,6 +746,10 @@ module ControlFlow {
746746 result = TSelf ( any ( Completion c | c .isValidFor ( cfe ) ) )
747747 }
748748
749+ private TRec specificBoolean ( boolean value ) {
750+ result = TRec ( TLastRecSpecificCompletion ( any ( BooleanCompletion bc | bc .getValue ( ) = value ) ) )
751+ }
752+
749753 /**
750754 * Gets an element from which the last element of `cfe` can be computed
751755 * (recursively) based on computation specification `c`. The predicate
@@ -788,7 +792,7 @@ module ControlFlow {
788792 cfe = any ( LogicalAndExpr lae |
789793 // Left operand exits with a false completion
790794 result = lae .getLeftOperand ( ) and
791- c = TRec ( TLastRecSpecificCompletion ( any ( FalseCompletion fc ) ) )
795+ c = specificBoolean ( false )
792796 or
793797 // Left operand exits abnormally
794798 result = lae .getLeftOperand ( ) and
@@ -802,7 +806,7 @@ module ControlFlow {
802806 cfe = any ( LogicalOrExpr loe |
803807 // Left operand exits with a true completion
804808 result = loe .getLeftOperand ( ) and
805- c = TRec ( TLastRecSpecificCompletion ( any ( TrueCompletion tc ) ) )
809+ c = specificBoolean ( true )
806810 or
807811 // Left operand exits abnormally
808812 result = loe .getLeftOperand ( ) and
@@ -887,7 +891,7 @@ module ControlFlow {
887891 cfe = any ( IfStmt is |
888892 // Condition exits with a false completion and there is no `else` branch
889893 result = is .getCondition ( ) and
890- c = TRec ( TLastRecSpecificCompletion ( any ( FalseCompletion fc ) ) ) and
894+ c = specificBoolean ( false ) and
891895 not exists ( is .getElse ( ) )
892896 or
893897 // Condition exits abnormally
@@ -936,7 +940,7 @@ module ControlFlow {
936940 c = TRec ( TLastRecSpecificNegCompletion ( any ( MatchingCompletion mc | mc .isMatch ( ) ) ) )
937941 or
938942 result = cs .getCondition ( ) and
939- c = TRec ( TLastRecSpecificCompletion ( any ( FalseCompletion fc ) ) )
943+ c = specificBoolean ( false )
940944 )
941945 or
942946 // Last statement exits with any non-break completion
@@ -966,7 +970,7 @@ module ControlFlow {
966970 cfe = any ( Case case |
967971 // Condition exists with a `false` completion
968972 result = case .getCondition ( ) and
969- c = TRec ( TLastRecSpecificCompletion ( any ( FalseCompletion fc ) ) )
973+ c = specificBoolean ( false )
970974 or
971975 // Condition exists abnormally
972976 result = case .getCondition ( ) and
@@ -987,7 +991,7 @@ module ControlFlow {
987991 |
988992 // Condition exits with a false completion
989993 result = ls .getCondition ( ) and
990- c = TRec ( TLastRecSpecificCompletion ( any ( FalseCompletion fc ) ) )
994+ c = specificBoolean ( false )
991995 or
992996 // Condition exits abnormally
993997 result = ls .getCondition ( ) and
@@ -1046,7 +1050,7 @@ module ControlFlow {
10461050 or
10471051 // Incompatible filter
10481052 result = scc .getFilterClause ( ) and
1049- c = TRec ( TLastRecSpecificCompletion ( any ( FalseCompletion fc ) ) )
1053+ c = specificBoolean ( false )
10501054 )
10511055 )
10521056 or
0 commit comments