@@ -520,6 +520,13 @@ module VariableCapture {
520
520
Flow:: storeStep ( closureNodeFrom , v , closureNodeTo )
521
521
}
522
522
523
+ predicate unmappedFlowStoreStep (
524
+ Flow:: ClosureNode closureNodeFrom , CapturedVariable v , Flow:: ClosureNode closureNodeTo
525
+ ) {
526
+ Flow:: storeStep ( closureNodeFrom , v , closureNodeTo ) and
527
+ not flowStoreStep ( _, closureNodeFrom , v , closureNodeTo , _)
528
+ }
529
+
523
530
predicate flowReadStep (
524
531
Node nodeFrom , Flow:: ClosureNode closureNodeFrom , CapturedVariable v ,
525
532
Flow:: ClosureNode closureNodeTo , Node nodeTo
@@ -529,13 +536,26 @@ module VariableCapture {
529
536
Flow:: readStep ( closureNodeFrom , v , closureNodeTo )
530
537
}
531
538
539
+ predicate unmappedFlowReadStep (
540
+ Flow:: ClosureNode closureNodeFrom , CapturedVariable v , Flow:: ClosureNode closureNodeTo
541
+ ) {
542
+ Flow:: readStep ( closureNodeFrom , v , closureNodeTo ) and
543
+ not flowReadStep ( _, closureNodeFrom , v , closureNodeTo , _)
544
+ }
545
+
532
546
predicate flowValueStep (
533
547
Node nodeFrom , Flow:: ClosureNode closureNodeFrom , Flow:: ClosureNode closureNodeTo , Node nodeTo
534
548
) {
535
549
closureNodeFrom = asClosureNode ( nodeFrom ) and
536
550
closureNodeTo = asClosureNode ( nodeTo ) and
537
551
Flow:: localFlowStep ( closureNodeFrom , closureNodeTo )
538
552
}
553
+
554
+ predicate unmappedFlowValueStep (
555
+ Flow:: ClosureNode closureNodeFrom , Flow:: ClosureNode closureNodeTo
556
+ ) {
557
+ Flow:: localFlowStep ( closureNodeFrom , closureNodeTo ) and
558
+ not flowValueStep ( _, closureNodeFrom , closureNodeTo , _)
539
559
}
540
560
}
541
561
0 commit comments