Module SsaImpl::SsaDefReaches

The construction of SSA form ensures that each use of a variable is dominated by its definition. A definition of an SSA variable therefore reaches a ControlFlowNode if it is the closest SSA variable definition that dominates the node. If two definitions dominate a node then one must dominate the other, so therefore the definition of closest is given by the dominator tree. Thus, reaching definitions can be calculated in terms of dominance.

Import path

import semmle.code.java.dataflow.SSA

Predicates

ssaDefReachesCapture	Holds if the SSA definition of `v` at `def` reaches capture point of `closurevar` without crossing another SSA definition of `v`.
ssaDefReachesEndOfBlock	Holds if the SSA definition of `v` at `def` reaches the end of a basic block `b`, at which point it is still live, without crossing another SSA definition of `v`.
ssaDefReachesUncertainDef	Holds if the SSA definition of `v` at `def` reaches `redef` without crossing another SSA definition of `v`.
ssaDefReachesUse	Holds if the SSA definition of `v` at `def` reaches `use` without crossing another SSA definition of `v`.