@@ -17,14 +17,10 @@ module ModulusAnalysis<
1717 LocationSig Location, Semantic Sem, DeltaSig D, BoundSig< Location , Sem , D > Bounds,
1818 UtilSig< Sem , D > U>
1919{
20- pragma [ nomagic]
21- private predicate valueFlowStepSsaEqFlowCond (
22- Sem:: SsaReadPosition pos , Sem:: SsaVariable v , Sem:: Expr e , int delta
23- ) {
24- exists ( Sem:: Guard guard , boolean testIsTrue |
25- guard = U:: semEqFlowCond ( v , e , D:: fromInt ( delta ) , true , testIsTrue ) and
26- Sem:: guardDirectlyControlsSsaRead ( guard , pos , testIsTrue )
27- )
20+ bindingset [ pos, v]
21+ pragma [ inline_late]
22+ private predicate hasReadOfVarInlineLate ( Sem:: SsaReadPosition pos , Sem:: SsaVariable v ) {
23+ pos .hasReadOfVar ( v )
2824 }
2925
3026 /**
@@ -36,8 +32,11 @@ module ModulusAnalysis<
3632 ) {
3733 U:: semSsaUpdateStep ( v , e , D:: fromInt ( delta ) ) and pos .hasReadOfVar ( v )
3834 or
39- pos .hasReadOfVar ( v ) and
40- valueFlowStepSsaEqFlowCond ( pos , v , e , delta )
35+ exists ( Sem:: Guard guard , boolean testIsTrue |
36+ hasReadOfVarInlineLate ( pos , v ) and
37+ guard = U:: semEqFlowCond ( v , e , D:: fromInt ( delta ) , true , testIsTrue ) and
38+ Sem:: guardDirectlyControlsSsaRead ( guard , pos , testIsTrue )
39+ )
4140 }
4241
4342 /**
0 commit comments