@@ -527,15 +527,20 @@ module FinallySplitting {
527
527
override string toString ( ) { result = "Finally (" + nestLevel + ")" }
528
528
}
529
529
530
+ pragma [ noinline]
531
+ private predicate hasEntry0 (
532
+ ControlFlowElement pred , FinallyControlFlowElement succ , int nestLevel , Completion c
533
+ ) {
534
+ succ .isEntryNode ( ) and
535
+ nestLevel = nestLevel ( succ .getTryStmt ( ) ) and
536
+ succ = succ ( pred , c )
537
+ }
538
+
530
539
private class FinallySplitInternal extends SplitInternal , FinallySplitImpl {
531
540
override FinallySplitKind getKind ( ) { result .getNestLevel ( ) = this .getNestLevel ( ) }
532
541
533
542
override predicate hasEntry ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
534
- succ = any ( FinallyControlFlowElement entry |
535
- entry .isEntryNode ( ) and
536
- this .getNestLevel ( ) = nestLevel ( entry .getTryStmt ( ) )
537
- ) and
538
- succ = succ ( pred , c ) and
543
+ hasEntry0 ( pred , succ , this .getNestLevel ( ) , c ) and
539
544
this .getType ( ) .isSplitForEntryCompletion ( c )
540
545
}
541
546
@@ -550,17 +555,22 @@ module FinallySplitting {
550
555
( exists ( succ ( pred , _) ) or exists ( succExit ( pred , _) ) )
551
556
}
552
557
558
+ pragma [ noinline]
559
+ private predicate exit0 ( ControlFlowElement pred , TryStmt try , int nestLevel , Completion c ) {
560
+ this .appliesToPredecessor ( pred ) and
561
+ nestLevel = nestLevel ( try ) and
562
+ pred = last ( try , c )
563
+ }
564
+
553
565
/**
554
566
* Holds if `pred` may exit this split with completion `c`. The Boolean
555
567
* `inherited` indicates whether `c` is an inherited completion from a `try`/
556
568
* `catch` block.
557
569
*/
558
570
private predicate exit ( ControlFlowElement pred , Completion c , boolean inherited ) {
559
- this .appliesToPredecessor ( pred ) and
560
571
exists ( TryStmt try , FinallySplitType type |
561
- type = this .getType ( ) and
562
- nestLevel ( try ) = this .getNestLevel ( ) and
563
- pred = last ( try , c )
572
+ exit0 ( pred , try , this .getNestLevel ( ) , c ) and
573
+ type = this .getType ( )
564
574
|
565
575
if pred = last ( try .getFinally ( ) , c )
566
576
then
@@ -1019,13 +1029,21 @@ module BooleanSplitting {
1019
1029
override string toString ( ) { result = kind .toString ( ) }
1020
1030
}
1021
1031
1032
+ pragma [ noinline]
1033
+ private predicate hasEntry0 (
1034
+ ControlFlowElement pred , ControlFlowElement succ , BooleanSplitSubKind kind , boolean b ,
1035
+ Completion c
1036
+ ) {
1037
+ kind .startsSplit ( pred ) and
1038
+ succ = succ ( pred , c ) and
1039
+ b = c .getInnerCompletion ( ) .( BooleanCompletion ) .getValue ( )
1040
+ }
1041
+
1022
1042
private class BooleanSplitInternal extends SplitInternal , BooleanSplitImpl {
1023
1043
override BooleanSplitKind getKind ( ) { result .getSubKind ( ) = this .getSubKind ( ) }
1024
1044
1025
1045
override predicate hasEntry ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1026
- succ = succ ( pred , c ) and
1027
- this .getSubKind ( ) .startsSplit ( pred ) and
1028
- this .getBranch ( ) = c .getInnerCompletion ( ) .( BooleanCompletion ) .getValue ( )
1046
+ hasEntry0 ( pred , succ , this .getSubKind ( ) , this .getBranch ( ) , c )
1029
1047
}
1030
1048
1031
1049
override predicate hasEntry ( Callable c , ControlFlowElement succ ) { none ( ) }
0 commit comments