@@ -17,14 +17,10 @@ module ModulusAnalysis<
17
17
LocationSig Location, Semantic Sem, DeltaSig D, BoundSig< Location , Sem , D > Bounds,
18
18
UtilSig< Sem , D > U>
19
19
{
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 )
28
24
}
29
25
30
26
/**
@@ -36,8 +32,11 @@ module ModulusAnalysis<
36
32
) {
37
33
U:: semSsaUpdateStep ( v , e , D:: fromInt ( delta ) ) and pos .hasReadOfVar ( v )
38
34
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
+ )
41
40
}
42
41
43
42
/**
0 commit comments