@@ -87,6 +87,10 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
87
87
)
88
88
}
89
89
90
+ private predicate uniqStepNotNull ( FlowNode n1 , FlowNode n2 ) {
91
+ uniqStep ( n1 , n2 ) and not isNull ( n1 )
92
+ }
93
+
90
94
private import Internal
91
95
92
96
module Internal {
@@ -100,7 +104,9 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
100
104
* Holds if data can flow from `n1` to `n2` in one step, excluding join
101
105
* steps from nodes that are always null.
102
106
*/
103
- predicate anyStep ( FlowNode n1 , FlowNode n2 ) { joinStepNotNull ( n1 , n2 ) or uniqStep ( n1 , n2 ) }
107
+ predicate anyStep ( FlowNode n1 , FlowNode n2 ) {
108
+ joinStepNotNull ( n1 , n2 ) or uniqStepNotNull ( n1 , n2 )
109
+ }
104
110
}
105
111
106
112
private predicate sccEdge ( FlowNode n1 , FlowNode n2 ) { anyStep ( n1 , n2 ) and anyStep + ( n2 , n1 ) }
@@ -250,7 +256,7 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
250
256
or
251
257
not P:: barrier ( n ) and
252
258
(
253
- exists ( FlowNode mid | hasProperty ( mid ) and uniqStep ( mid , n ) )
259
+ exists ( FlowNode mid | hasProperty ( mid ) and uniqStepNotNull ( mid , n ) )
254
260
or
255
261
// The following is an optimized version of
256
262
// `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
@@ -298,7 +304,7 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
298
304
or
299
305
not P:: barrier ( n ) and
300
306
(
301
- exists ( FlowNode mid | hasProperty ( mid , t ) and uniqStep ( mid , n ) )
307
+ exists ( FlowNode mid | hasProperty ( mid , t ) and uniqStepNotNull ( mid , n ) )
302
308
or
303
309
// The following is an optimized version of
304
310
// `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
0 commit comments