@@ -51,27 +51,23 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
5151 private predicate isNull ( FlowNode n ) {
5252 isNullValue ( n )
5353 or
54- exists ( FlowNode mid | isNull ( mid ) and uniqStep ( mid , n ) )
55- or
56- forex ( FlowNode mid | joinStep ( mid , n ) | isNull ( mid ) ) and
57- not isExcludedFromNullAnalysis ( n )
54+ not isExcludedFromNullAnalysis ( n ) and
55+ (
56+ exists ( FlowNode mid | isNull ( mid ) and uniqStep ( mid , n ) )
57+ or
58+ forex ( FlowNode mid | joinStep ( mid , n ) | isNull ( mid ) )
59+ )
5860 }
5961
6062 /**
6163 * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
6264 * functionally determined by `n2`, and `n1` might take a non-null value.
6365 */
64- predicate joinStepNotNull ( FlowNode n1 , FlowNode n2 ) {
65- joinStep ( n1 , n2 ) and not isNull ( n1 )
66- }
66+ predicate joinStepNotNull ( FlowNode n1 , FlowNode n2 ) { joinStep ( n1 , n2 ) and not isNull ( n1 ) }
6767
68- predicate anyStep ( FlowNode n1 , FlowNode n2 ) {
69- joinStepNotNull ( n1 , n2 ) or uniqStep ( n1 , n2 )
70- }
68+ predicate anyStep ( FlowNode n1 , FlowNode n2 ) { joinStepNotNull ( n1 , n2 ) or uniqStep ( n1 , n2 ) }
7169
72- private predicate sccEdge ( FlowNode n1 , FlowNode n2 ) {
73- anyStep ( n1 , n2 ) and anyStep + ( n2 , n1 )
74- }
70+ private predicate sccEdge ( FlowNode n1 , FlowNode n2 ) { anyStep ( n1 , n2 ) and anyStep + ( n2 , n1 ) }
7571
7672 private module Scc = QlBuiltins:: EquivalenceRelation< FlowNode , sccEdge / 2 > ;
7773
@@ -281,4 +277,4 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
281277 )
282278 }
283279 }
284- }
280+ }
0 commit comments