@@ -164,7 +164,7 @@ private predicate uncertainVariableUpdateImpl(TrackedVar v, ControlFlowNode n, B
164164predicate uncertainVariableUpdate ( TrackedVar v , ControlFlowNode n , BasicBlock b , int i ) =
165165 forceLocal( uncertainVariableUpdateImpl / 4 ) ( v , n , b , i )
166166
167- private module SsaInput implements SsaImplCommon:: InputSig< Location , BasicBlock > {
167+ private module SsaImplInput implements SsaImplCommon:: InputSig< Location , BasicBlock > {
168168 class SourceVariable = SsaSourceVariable ;
169169
170170 /**
@@ -206,7 +206,35 @@ private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock>
206206 }
207207}
208208
209- import SsaImplCommon:: Make< Location , Cfg , SsaInput > as Impl
209+ import SsaImplCommon:: Make< Location , Cfg , SsaImplInput > as Impl
210+
211+ private module SsaInput implements Impl:: SsaInputSig {
212+ private import java as J
213+
214+ class Expr = J:: Expr ;
215+
216+ class Parameter = J:: Parameter ;
217+
218+ class VariableWrite = J:: VariableWrite ;
219+
220+ predicate explicitWrite ( VariableWrite w , BasicBlock bb , int i , SsaSourceVariable v ) {
221+ exists ( VariableUpdate upd |
222+ upd = w .asExpr ( ) and
223+ certainVariableUpdate ( v , upd .getControlFlowNode ( ) , bb , i ) and
224+ getDestVar ( upd ) = v
225+ )
226+ or
227+ exists ( Parameter p , Callable c |
228+ c = p .getCallable ( ) and
229+ v = TLocalVar ( c , p ) and
230+ w .isParameterInit ( p ) and
231+ c .getBody ( ) .getBasicBlock ( ) = bb and
232+ i = - 1
233+ )
234+ }
235+ }
236+
237+ module Ssa = Impl:: MakeSsa< SsaInput > ;
210238
211239final class Definition = Impl:: Definition ;
212240
0 commit comments