diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll b/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll index adcfdfaaca7..899165f5f34 100644 --- a/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll +++ b/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll @@ -706,9 +706,9 @@ module Ssa { /** * Holds if `def` is accessed in basic block `bb1` (either a read or a write), - * `bb2` is a transitive successor of `bb1`, and `def` is *maybe* read in `bb2` - * or one of its transitive successors, but not in any block on the path between - * `bb1` and `bb2`. + * `bb2` is a transitive successor of `bb1`, `def` is live at the end of `bb1`, + * and the underlying variable for `def` is neither read nor written in any block + * on the path between `bb1` and `bb2`. */ private predicate varBlockReaches(TrackedDefinition def, BasicBlock bb1, BasicBlock bb2) { varOccursInBlock(def, bb1, _) and diff --git a/java/ql/src/semmle/code/java/dataflow/SSA.qll b/java/ql/src/semmle/code/java/dataflow/SSA.qll index 84d6f179efb..851427c4b26 100644 --- a/java/ql/src/semmle/code/java/dataflow/SSA.qll +++ b/java/ql/src/semmle/code/java/dataflow/SSA.qll @@ -770,7 +770,9 @@ private module SsaImpl { /** Holds if `v` occurs in `b` or one of `b`'s transitive successors. */ private predicate blockPrecedesVar(TrackedVar v, BasicBlock b) { - varOccursInBlock(v, b.getABBSuccessor*()) + varOccursInBlock(v, b) + or + ssaDefReachesEndOfBlock(v, _, b) } /** diff --git a/java/ql/src/semmle/code/java/dataflow/internal/BaseSSA.qll b/java/ql/src/semmle/code/java/dataflow/internal/BaseSSA.qll index 9c911a2782c..58021120b5c 100644 --- a/java/ql/src/semmle/code/java/dataflow/internal/BaseSSA.qll +++ b/java/ql/src/semmle/code/java/dataflow/internal/BaseSSA.qll @@ -321,7 +321,9 @@ private module SsaImpl { /** Holds if `v` occurs in `b` or one of `b`'s transitive successors. */ private predicate blockPrecedesVar(BaseSsaSourceVariable v, BasicBlock b) { - varOccursInBlock(v, b.getABBSuccessor*()) + varOccursInBlock(v, b) + or + ssaDefReachesEndOfBlock(v, _, b) } /** diff --git a/python/ql/src/semmle/python/essa/SsaCompute.qll b/python/ql/src/semmle/python/essa/SsaCompute.qll index ad348675805..c9b4b28f96d 100644 --- a/python/ql/src/semmle/python/essa/SsaCompute.qll +++ b/python/ql/src/semmle/python/essa/SsaCompute.qll @@ -382,7 +382,9 @@ private module SsaComputeImpl { /** Holds if `v` occurs in `b` or one of `b`'s transitive successors. */ private predicate blockPrecedesVar(SsaSourceVariable v, BasicBlock b) { - varOccursInBlock(v, b.getASuccessor*()) + varOccursInBlock(v, b) + or + SsaDefinitionsImpl::reachesEndOfBlock(v, _, _, b) } /**