diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll
index f1bdd6b8c520..3cf15775b3bf 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll
@@ -136,7 +136,9 @@ private module SourceVariables {
     NormalSourceVariable() { this = TNormalSourceVariable(base, ind) }
 
     final override string toString() {
-      result = repeatStars(this.getIndirection()) + base.toString()
+      if ind = 0
+      then result = "&" + base.toString()
+      else result = repeatStars(this.getIndirection() - 1) + base.toString()
     }
   }
 
@@ -157,7 +159,9 @@ private module SourceVariables {
     }
 
     final override string toString() {
-      result = repeatStars(this.getIndirection()) + base.toString() + " [before crement]"
+      if ind = 0
+      then result = "&" + base.toString() + " [before crement]"
+      else result = repeatStars(this.getIndirection() - 1) + base.toString() + " [before crement]"
     }
 
     /**
@@ -1353,6 +1357,53 @@ class PhiNode extends Definition instanceof SsaImpl::PhiNode {
   final predicate hasInputFromBlock(Definition input, IRBlock bb) {
     phiHasInputFromBlock(this, input, bb)
   }
+
+  override int getIndirection() { result = this.getSourceVariable().getIndirection() }
+
+  override predicate isCertain() {
+    // If this phi node is part of a phi cycle of phi nodes the least
+    // fixed-point semantics of datalog means we don't get the right answer.
+    // So we perform an SCC reduction to simulate greated fixed-point semantics.
+    getCycle(this).isCertain()
+    or
+    // If there is no cycle we get the right semantics through traditional
+    // recursion.
+    not exists(getCycle(this)) and
+    forex(Definition inp | inp = this.getAnInput() | inp.isCertain())
+  }
+
+  final override Declaration getFunction() {
+    result = SsaImpl::PhiNode.super.getBasicBlock().getEnclosingFunction()
+  }
+}
+
+private PhiNode getAnInput(PhiNode phi) { result = phi.getAnInput() }
+
+private predicate definitionCycle(PhiNode phi) { getAnInput+(phi) = phi }
+
+private predicate hasAnInput(PhiNode phi1, PhiNode phi2) {
+  definitionCycle(phi1) and
+  definitionCycle(phi2) and
+  getAnInput(phi1) = phi2
+}
+
+private module PhiCycleEquivalence = QlBuiltins::EquivalenceRelation<PhiNode, hasAnInput/2>;
+
+private PhiCycle getCycle(PhiNode phi) { result.getAPhiNode() = phi }
+
+private class PhiCycle extends PhiCycleEquivalence::EquivalenceClass {
+  PhiNode getAPhiNode() { PhiCycleEquivalence::getEquivalenceClass(result) = this }
+
+  predicate hasPhiNode(PhiNode phi) { this.getAPhiNode() = phi }
+
+  string toString() { result = strictconcat(this.getAPhiNode().toString(), ", ") }
+
+  predicate isCertain() {
+    // A phi cycle is certain if all of the inputs into the phi cycle is certain.
+    forex(PhiNode phi | phi = this.getAPhiNode() |
+      forall(PhiNode inp | phi.getAnInput() = inp and not this.hasPhiNode(inp) | inp.isCertain())
+    )
+  }
 }
 
 /** An static single assignment (SSA) definition. */
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll
index e4734f285fa7..31931189003c 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll
@@ -147,7 +147,7 @@ abstract class Indirection extends Type {
    *
    * `certain` is `true` if this write is guaranteed to write to the address.
    */
-  predicate isAdditionalWrite(Node0Impl value, Operand address, boolean certain) { none() }
+  predicate isAdditionalWrite(Node0Impl value, Operand address, Certainty certain) { none() }
 
   /**
    * Gets the base type of this indirection, after specifiers have been deeply
@@ -198,11 +198,11 @@ private module IteratorIndirections {
       baseType = super.getValueType()
     }
 
-    override predicate isAdditionalWrite(Node0Impl value, Operand address, boolean certain) {
+    override predicate isAdditionalWrite(Node0Impl value, Operand address, Certainty certain) {
       exists(CallInstruction call | call.getArgumentOperand(0) = value.asOperand() |
         this = call.getStaticCallTarget().(Function).getClassAndName("operator=") and
         address = call.getThisArgumentOperand() and
-        certain = false
+        certain instanceof AlwaysUncertain
       )
     }
 
@@ -271,30 +271,62 @@ predicate isDereference(Instruction deref, Operand address, boolean additional)
   additional = false
 }
 
-predicate isWrite(Node0Impl value, Operand address, boolean certain) {
+private newtype TCertainty =
+  TCertainWhenAddressIsCertain() or
+  TAlwaysCertain() or
+  TAlwaysUncertain()
+
+abstract private class Certainty extends TCertainty {
+  abstract predicate isCertain(boolean addressIsCertain);
+
+  abstract string toString();
+}
+
+private class CertainWhenAddressIsCertain extends Certainty, TCertainWhenAddressIsCertain {
+  override predicate isCertain(boolean addressIsCertain) { addressIsCertain = true }
+
+  override string toString() { result = "CertainWhenAddressIsCertain" }
+}
+
+private class AlwaysCertain extends Certainty, TAlwaysCertain {
+  override predicate isCertain(boolean addressIsCertain) {
+    addressIsCertain = true or addressIsCertain = false
+  }
+
+  override string toString() { result = "AlwaysCertain" }
+}
+
+private class AlwaysUncertain extends Certainty, TAlwaysUncertain {
+  override predicate isCertain(boolean addressIsCertain) { none() }
+
+  override string toString() { result = "AlwaysUncertain" }
+}
+
+predicate isWrite(Node0Impl value, Operand address, Certainty certain) {
   any(Indirection ind).isAdditionalWrite(value, address, certain)
   or
-  certain = true and
-  (
-    exists(StoreInstruction store |
-      value.asInstruction() = store and
-      address = store.getDestinationAddressOperand()
-    )
-    or
-    exists(InitializeParameterInstruction init |
-      value.asInstruction() = init and
-      address = init.getAnOperand()
-    )
-    or
-    exists(InitializeDynamicAllocationInstruction init |
-      value.asInstruction() = init and
-      address = init.getAllocationAddressOperand()
-    )
-    or
-    exists(UninitializedInstruction uninitialized |
-      value.asInstruction() = uninitialized and
-      address = uninitialized.getAnOperand()
-    )
+  exists(StoreInstruction store |
+    value.asInstruction() = store and
+    address = store.getDestinationAddressOperand() and
+    certain instanceof CertainWhenAddressIsCertain
+  )
+  or
+  exists(InitializeParameterInstruction init |
+    value.asInstruction() = init and
+    address = init.getAnOperand() and
+    certain instanceof AlwaysCertain
+  )
+  or
+  exists(InitializeDynamicAllocationInstruction init |
+    value.asInstruction() = init and
+    address = init.getAllocationAddressOperand() and
+    certain instanceof AlwaysCertain
+  )
+  or
+  exists(UninitializedInstruction uninitialized |
+    value.asInstruction() = uninitialized and
+    address = uninitialized.getAnOperand() and
+    certain instanceof AlwaysCertain
   )
 }
 
@@ -718,16 +750,18 @@ private module Cached {
     int indirectionIndex
   ) {
     exists(
-      boolean writeIsCertain, boolean addressIsCertain, int ind0, CppType type, int lower, int upper
+      Certainty writeIsCertain, boolean addressIsCertain, int ind0, CppType type, int lower,
+      int upper
     |
       isWrite(value, address, writeIsCertain) and
       isDefImpl(address, base, ind0, addressIsCertain) and
-      certain = writeIsCertain.booleanAnd(addressIsCertain) and
       type = getLanguageType(address) and
       upper = countIndirectionsForCppType(type) and
       ind = ind0 + [lower .. upper] and
       indirectionIndex = ind - (ind0 + lower) and
       lower = getMinIndirectionsForType(any(Type t | type.hasUnspecifiedType(t, _)))
+    |
+      if writeIsCertain.isCertain(addressIsCertain) then certain = true else certain = false
     )
   }
 
diff --git a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
index a9927b510930..a4c154c06940 100644
--- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
+++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
@@ -21,11 +21,7 @@ edges
 | test.cpp:85:21:85:36 | buf | test.cpp:87:5:87:31 | access to array | provenance | Config |
 | test.cpp:85:21:85:36 | buf | test.cpp:88:5:88:27 | access to array | provenance | Config |
 | test.cpp:85:34:85:36 | buf | test.cpp:85:21:85:36 | buf | provenance |  |
-| test.cpp:92:9:92:11 | definition of arr | test.cpp:96:13:96:18 | access to array | provenance | Config |
 | test.cpp:96:13:96:15 | arr | test.cpp:96:13:96:18 | access to array | provenance | Config |
-| test.cpp:102:9:102:11 | definition of arr | test.cpp:111:17:111:22 | access to array | provenance | Config |
-| test.cpp:102:9:102:11 | definition of arr | test.cpp:115:35:115:40 | access to array | provenance | Config |
-| test.cpp:102:9:102:11 | definition of arr | test.cpp:119:17:119:22 | access to array | provenance | Config |
 | test.cpp:111:17:111:19 | arr | test.cpp:111:17:111:22 | access to array | provenance | Config |
 | test.cpp:111:17:111:19 | arr | test.cpp:115:35:115:40 | access to array | provenance | Config |
 | test.cpp:111:17:111:19 | arr | test.cpp:119:17:119:22 | access to array | provenance | Config |
@@ -35,55 +31,41 @@ edges
 | test.cpp:119:17:119:19 | arr | test.cpp:111:17:111:22 | access to array | provenance | Config |
 | test.cpp:119:17:119:19 | arr | test.cpp:115:35:115:40 | access to array | provenance | Config |
 | test.cpp:119:17:119:19 | arr | test.cpp:119:17:119:22 | access to array | provenance | Config |
-| test.cpp:125:11:125:13 | definition of arr | test.cpp:128:9:128:14 | access to array | provenance | Config |
 | test.cpp:128:9:128:11 | arr | test.cpp:128:9:128:14 | access to array | provenance | Config |
 | test.cpp:134:25:134:27 | arr | test.cpp:136:9:136:16 | ... += ... | provenance | Config |
 | test.cpp:136:9:136:16 | ... += ... | test.cpp:136:9:136:16 | ... += ... | provenance |  |
 | test.cpp:136:9:136:16 | ... += ... | test.cpp:138:13:138:15 | arr | provenance |  |
-| test.cpp:142:10:142:13 | definition of asdf | test.cpp:143:18:143:21 | asdf | provenance |  |
 | test.cpp:143:18:143:21 | asdf | test.cpp:134:25:134:27 | arr | provenance |  |
 | test.cpp:143:18:143:21 | asdf | test.cpp:143:18:143:21 | asdf | provenance |  |
 | test.cpp:146:26:146:26 | *p | test.cpp:147:4:147:9 | -- ... | provenance |  |
 | test.cpp:146:26:146:26 | *p | test.cpp:147:4:147:9 | -- ... | provenance |  |
-| test.cpp:154:7:154:9 | definition of buf | test.cpp:156:12:156:18 | ... + ... | provenance | Config |
 | test.cpp:156:12:156:14 | buf | test.cpp:156:12:156:18 | ... + ... | provenance | Config |
 | test.cpp:156:12:156:18 | ... + ... | test.cpp:156:12:156:18 | ... + ... | provenance |  |
 | test.cpp:156:12:156:18 | ... + ... | test.cpp:158:17:158:18 | *& ... | provenance |  |
 | test.cpp:158:17:158:18 | *& ... | test.cpp:146:26:146:26 | *p | provenance |  |
-| test.cpp:217:19:217:24 | definition of buffer | test.cpp:218:16:218:28 | buffer | provenance |  |
 | test.cpp:218:16:218:28 | buffer | test.cpp:220:5:220:11 | access to array | provenance | Config |
 | test.cpp:218:16:218:28 | buffer | test.cpp:221:5:221:11 | access to array | provenance | Config |
 | test.cpp:218:23:218:28 | buffer | test.cpp:218:16:218:28 | buffer | provenance |  |
-| test.cpp:228:10:228:14 | definition of array | test.cpp:229:17:229:29 | array | provenance |  |
 | test.cpp:229:17:229:29 | array | test.cpp:231:5:231:10 | access to array | provenance | Config |
 | test.cpp:229:17:229:29 | array | test.cpp:232:5:232:10 | access to array | provenance | Config |
 | test.cpp:229:25:229:29 | array | test.cpp:229:17:229:29 | array | provenance |  |
 | test.cpp:245:30:245:30 | p | test.cpp:261:27:261:30 | access to array | provenance | Config |
 | test.cpp:245:30:245:30 | p | test.cpp:261:27:261:30 | access to array | provenance | Config |
-| test.cpp:273:19:273:25 | definition of buffer3 | test.cpp:274:14:274:20 | buffer3 | provenance |  |
 | test.cpp:274:14:274:20 | buffer3 | test.cpp:245:30:245:30 | p | provenance |  |
 | test.cpp:274:14:274:20 | buffer3 | test.cpp:274:14:274:20 | buffer3 | provenance |  |
 | test.cpp:277:35:277:35 | p | test.cpp:278:14:278:14 | p | provenance |  |
 | test.cpp:278:14:278:14 | p | test.cpp:245:30:245:30 | p | provenance |  |
-| test.cpp:282:19:282:25 | definition of buffer1 | test.cpp:283:19:283:25 | buffer1 | provenance |  |
 | test.cpp:283:19:283:25 | buffer1 | test.cpp:277:35:277:35 | p | provenance |  |
 | test.cpp:283:19:283:25 | buffer1 | test.cpp:283:19:283:25 | buffer1 | provenance |  |
-| test.cpp:285:19:285:25 | definition of buffer2 | test.cpp:286:19:286:25 | buffer2 | provenance |  |
 | test.cpp:286:19:286:25 | buffer2 | test.cpp:277:35:277:35 | p | provenance |  |
 | test.cpp:286:19:286:25 | buffer2 | test.cpp:286:19:286:25 | buffer2 | provenance |  |
-| test.cpp:288:19:288:25 | definition of buffer3 | test.cpp:289:19:289:25 | buffer3 | provenance |  |
 | test.cpp:289:19:289:25 | buffer3 | test.cpp:277:35:277:35 | p | provenance |  |
 | test.cpp:289:19:289:25 | buffer3 | test.cpp:289:19:289:25 | buffer3 | provenance |  |
 | test.cpp:292:25:292:27 | arr | test.cpp:299:16:299:21 | access to array | provenance | Config |
-| test.cpp:305:9:305:12 | definition of arr1 | test.cpp:306:20:306:23 | arr1 | provenance |  |
 | test.cpp:306:20:306:23 | arr1 | test.cpp:292:25:292:27 | arr | provenance |  |
 | test.cpp:306:20:306:23 | arr1 | test.cpp:306:20:306:23 | arr1 | provenance |  |
-| test.cpp:308:9:308:12 | definition of arr2 | test.cpp:309:20:309:23 | arr2 | provenance |  |
 | test.cpp:309:20:309:23 | arr2 | test.cpp:292:25:292:27 | arr | provenance |  |
 | test.cpp:309:20:309:23 | arr2 | test.cpp:309:20:309:23 | arr2 | provenance |  |
-| test.cpp:314:10:314:13 | definition of temp | test.cpp:319:19:319:27 | ... + ... | provenance | Config |
-| test.cpp:314:10:314:13 | definition of temp | test.cpp:322:19:322:27 | ... + ... | provenance | Config |
-| test.cpp:314:10:314:13 | definition of temp | test.cpp:324:23:324:32 | ... + ... | provenance | Config |
 | test.cpp:319:13:319:27 | ... = ... | test.cpp:325:24:325:26 | end | provenance |  |
 | test.cpp:319:19:319:22 | temp | test.cpp:319:19:319:27 | ... + ... | provenance | Config |
 | test.cpp:319:19:319:22 | temp | test.cpp:324:23:324:32 | ... + ... | provenance | Config |
@@ -133,40 +115,33 @@ nodes
 | test.cpp:85:34:85:36 | buf | semmle.label | buf |
 | test.cpp:87:5:87:31 | access to array | semmle.label | access to array |
 | test.cpp:88:5:88:27 | access to array | semmle.label | access to array |
-| test.cpp:92:9:92:11 | definition of arr | semmle.label | definition of arr |
 | test.cpp:96:13:96:15 | arr | semmle.label | arr |
 | test.cpp:96:13:96:18 | access to array | semmle.label | access to array |
-| test.cpp:102:9:102:11 | definition of arr | semmle.label | definition of arr |
 | test.cpp:111:17:111:19 | arr | semmle.label | arr |
 | test.cpp:111:17:111:22 | access to array | semmle.label | access to array |
 | test.cpp:115:35:115:37 | arr | semmle.label | arr |
 | test.cpp:115:35:115:40 | access to array | semmle.label | access to array |
 | test.cpp:119:17:119:19 | arr | semmle.label | arr |
 | test.cpp:119:17:119:22 | access to array | semmle.label | access to array |
-| test.cpp:125:11:125:13 | definition of arr | semmle.label | definition of arr |
 | test.cpp:128:9:128:11 | arr | semmle.label | arr |
 | test.cpp:128:9:128:14 | access to array | semmle.label | access to array |
 | test.cpp:134:25:134:27 | arr | semmle.label | arr |
 | test.cpp:136:9:136:16 | ... += ... | semmle.label | ... += ... |
 | test.cpp:136:9:136:16 | ... += ... | semmle.label | ... += ... |
 | test.cpp:138:13:138:15 | arr | semmle.label | arr |
-| test.cpp:142:10:142:13 | definition of asdf | semmle.label | definition of asdf |
 | test.cpp:143:18:143:21 | asdf | semmle.label | asdf |
 | test.cpp:143:18:143:21 | asdf | semmle.label | asdf |
 | test.cpp:146:26:146:26 | *p | semmle.label | *p |
 | test.cpp:147:4:147:9 | -- ... | semmle.label | -- ... |
 | test.cpp:147:4:147:9 | -- ... | semmle.label | -- ... |
-| test.cpp:154:7:154:9 | definition of buf | semmle.label | definition of buf |
 | test.cpp:156:12:156:14 | buf | semmle.label | buf |
 | test.cpp:156:12:156:18 | ... + ... | semmle.label | ... + ... |
 | test.cpp:156:12:156:18 | ... + ... | semmle.label | ... + ... |
 | test.cpp:158:17:158:18 | *& ... | semmle.label | *& ... |
-| test.cpp:217:19:217:24 | definition of buffer | semmle.label | definition of buffer |
 | test.cpp:218:16:218:28 | buffer | semmle.label | buffer |
 | test.cpp:218:23:218:28 | buffer | semmle.label | buffer |
 | test.cpp:220:5:220:11 | access to array | semmle.label | access to array |
 | test.cpp:221:5:221:11 | access to array | semmle.label | access to array |
-| test.cpp:228:10:228:14 | definition of array | semmle.label | definition of array |
 | test.cpp:229:17:229:29 | array | semmle.label | array |
 | test.cpp:229:25:229:29 | array | semmle.label | array |
 | test.cpp:231:5:231:10 | access to array | semmle.label | access to array |
@@ -174,29 +149,22 @@ nodes
 | test.cpp:245:30:245:30 | p | semmle.label | p |
 | test.cpp:245:30:245:30 | p | semmle.label | p |
 | test.cpp:261:27:261:30 | access to array | semmle.label | access to array |
-| test.cpp:273:19:273:25 | definition of buffer3 | semmle.label | definition of buffer3 |
 | test.cpp:274:14:274:20 | buffer3 | semmle.label | buffer3 |
 | test.cpp:274:14:274:20 | buffer3 | semmle.label | buffer3 |
 | test.cpp:277:35:277:35 | p | semmle.label | p |
 | test.cpp:278:14:278:14 | p | semmle.label | p |
-| test.cpp:282:19:282:25 | definition of buffer1 | semmle.label | definition of buffer1 |
 | test.cpp:283:19:283:25 | buffer1 | semmle.label | buffer1 |
 | test.cpp:283:19:283:25 | buffer1 | semmle.label | buffer1 |
-| test.cpp:285:19:285:25 | definition of buffer2 | semmle.label | definition of buffer2 |
 | test.cpp:286:19:286:25 | buffer2 | semmle.label | buffer2 |
 | test.cpp:286:19:286:25 | buffer2 | semmle.label | buffer2 |
-| test.cpp:288:19:288:25 | definition of buffer3 | semmle.label | definition of buffer3 |
 | test.cpp:289:19:289:25 | buffer3 | semmle.label | buffer3 |
 | test.cpp:289:19:289:25 | buffer3 | semmle.label | buffer3 |
 | test.cpp:292:25:292:27 | arr | semmle.label | arr |
 | test.cpp:299:16:299:21 | access to array | semmle.label | access to array |
-| test.cpp:305:9:305:12 | definition of arr1 | semmle.label | definition of arr1 |
 | test.cpp:306:20:306:23 | arr1 | semmle.label | arr1 |
 | test.cpp:306:20:306:23 | arr1 | semmle.label | arr1 |
-| test.cpp:308:9:308:12 | definition of arr2 | semmle.label | definition of arr2 |
 | test.cpp:309:20:309:23 | arr2 | semmle.label | arr2 |
 | test.cpp:309:20:309:23 | arr2 | semmle.label | arr2 |
-| test.cpp:314:10:314:13 | definition of temp | semmle.label | definition of temp |
 | test.cpp:319:13:319:27 | ... = ... | semmle.label | ... = ... |
 | test.cpp:319:19:319:22 | temp | semmle.label | temp |
 | test.cpp:319:19:319:27 | ... + ... | semmle.label | ... + ... |
@@ -221,25 +189,14 @@ subpaths
 | test.cpp:72:5:72:15 | PointerAdd: access to array | test.cpp:79:32:79:34 | buf | test.cpp:72:5:72:15 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:72:5:72:19 | Store: ... = ... | write |
 | test.cpp:77:27:77:44 | PointerAdd: access to array | test.cpp:77:32:77:34 | buf | test.cpp:66:32:66:32 | p | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:67:5:67:10 | Store: ... = ... | write |
 | test.cpp:88:5:88:27 | PointerAdd: access to array | test.cpp:85:34:85:36 | buf | test.cpp:88:5:88:27 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:88:5:88:31 | Store: ... = ... | write |
-| test.cpp:128:9:128:14 | PointerAdd: access to array | test.cpp:125:11:125:13 | definition of arr | test.cpp:128:9:128:14 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:125:11:125:13 | arr | arr | test.cpp:128:9:128:18 | Store: ... = ... | write |
 | test.cpp:128:9:128:14 | PointerAdd: access to array | test.cpp:128:9:128:11 | arr | test.cpp:128:9:128:14 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:125:11:125:13 | arr | arr | test.cpp:128:9:128:18 | Store: ... = ... | write |
-| test.cpp:136:9:136:16 | PointerAdd: ... += ... | test.cpp:142:10:142:13 | definition of asdf | test.cpp:138:13:138:15 | arr | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:142:10:142:13 | asdf | asdf | test.cpp:138:12:138:15 | Load: * ... | read |
 | test.cpp:136:9:136:16 | PointerAdd: ... += ... | test.cpp:143:18:143:21 | asdf | test.cpp:138:13:138:15 | arr | This pointer arithmetic may have an off-by-2 error allowing it to overrun $@ at this $@. | test.cpp:142:10:142:13 | asdf | asdf | test.cpp:138:12:138:15 | Load: * ... | read |
-| test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:154:7:154:9 | definition of buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
-| test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:154:7:154:9 | definition of buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
 | test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:156:12:156:14 | buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
 | test.cpp:156:12:156:18 | PointerAdd: ... + ... | test.cpp:156:12:156:14 | buf | test.cpp:147:4:147:9 | -- ... | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:154:7:154:9 | buf | buf | test.cpp:147:3:147:13 | Store: ... = ... | write |
-| test.cpp:221:5:221:11 | PointerAdd: access to array | test.cpp:217:19:217:24 | definition of buffer | test.cpp:221:5:221:11 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:217:19:217:24 | buffer | buffer | test.cpp:221:5:221:15 | Store: ... = ... | write |
 | test.cpp:221:5:221:11 | PointerAdd: access to array | test.cpp:218:23:218:28 | buffer | test.cpp:221:5:221:11 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:217:19:217:24 | buffer | buffer | test.cpp:221:5:221:15 | Store: ... = ... | write |
-| test.cpp:232:5:232:10 | PointerAdd: access to array | test.cpp:228:10:228:14 | definition of array | test.cpp:232:5:232:10 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:228:10:228:14 | array | array | test.cpp:232:5:232:19 | Store: ... = ... | write |
 | test.cpp:232:5:232:10 | PointerAdd: access to array | test.cpp:229:25:229:29 | array | test.cpp:232:5:232:10 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:228:10:228:14 | array | array | test.cpp:232:5:232:19 | Store: ... = ... | write |
-| test.cpp:261:27:261:30 | PointerAdd: access to array | test.cpp:285:19:285:25 | definition of buffer2 | test.cpp:261:27:261:30 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:285:19:285:25 | buffer2 | buffer2 | test.cpp:261:27:261:30 | Load: access to array | read |
 | test.cpp:261:27:261:30 | PointerAdd: access to array | test.cpp:286:19:286:25 | buffer2 | test.cpp:261:27:261:30 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:285:19:285:25 | buffer2 | buffer2 | test.cpp:261:27:261:30 | Load: access to array | read |
-| test.cpp:299:16:299:21 | PointerAdd: access to array | test.cpp:308:9:308:12 | definition of arr2 | test.cpp:299:16:299:21 | access to array | This pointer arithmetic may have an off-by-1014 error allowing it to overrun $@ at this $@. | test.cpp:308:9:308:12 | arr2 | arr2 | test.cpp:299:16:299:21 | Load: access to array | read |
 | test.cpp:299:16:299:21 | PointerAdd: access to array | test.cpp:309:20:309:23 | arr2 | test.cpp:299:16:299:21 | access to array | This pointer arithmetic may have an off-by-1014 error allowing it to overrun $@ at this $@. | test.cpp:308:9:308:12 | arr2 | arr2 | test.cpp:299:16:299:21 | Load: access to array | read |
-| test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:314:10:314:13 | definition of temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:330:13:330:24 | Store: ... = ... | write |
-| test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:314:10:314:13 | definition of temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:331:13:331:24 | Store: ... = ... | write |
-| test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:314:10:314:13 | definition of temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:333:13:333:24 | Store: ... = ... | write |
 | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:330:13:330:24 | Store: ... = ... | write |
 | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:331:13:331:24 | Store: ... = ... | write |
 | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:333:13:333:24 | Store: ... = ... | write |
diff --git a/cpp/ql/test/library-tests/dataflow/certain/test.cpp b/cpp/ql/test/library-tests/dataflow/certain/test.cpp
new file mode 100644
index 000000000000..8ec99673e908
--- /dev/null
+++ b/cpp/ql/test/library-tests/dataflow/certain/test.cpp
@@ -0,0 +1,64 @@
+void use(...);
+
+void test1() {
+  int x = 0; // $ certain="SSA def(&x)" certain="SSA def(x)"
+  use(x);
+
+  x = 1; // $ certain="SSA def(x)"
+  use(x);
+
+  int* p = &x; // $ certain="SSA def(&p)" certain="SSA def(p)" certain="SSA def(*p)"
+  use(p);
+
+  *p = 2; // $ certain="SSA def(*p)"
+  use(p);
+
+  p = nullptr; // $ certain="SSA def(p)" certain="SSA def(*p)"
+  use(p);
+
+  *p = 2; // $ uncertain="SSA def(*p)"
+  use(p);
+}
+
+void test2(bool b) { // $ certain="SSA def(&b)" certain="SSA def(b)"
+  {
+  int x; // $ certain="SSA def(&x)" 
+  if(b) {
+    x = 0; // $ certain="SSA def(x)"
+  } else {
+    x = 1; // $ certain="SSA def(x)"
+  }
+  use(x); // $ certain="SSA phi(x)"
+  }
+
+  {
+  int x; // $ certain="SSA def(&x)" certain="SSA def(x)"
+  if(b) {
+    x = 0; // $ certain="SSA def(x)"
+  } else {
+  
+  }
+  use(x); // $ certain="SSA phi(x)"
+  }
+
+  {
+  int x; // $ certain="SSA def(&x)" certain="SSA def(x)"
+  int* p = &x; // $ certain="SSA def(&p)" certain="SSA def(p)" certain="SSA def(*p)"
+  if(b) {
+    *p = 0; // $ certain="SSA def(*p)"
+  } else {
+    *(p + 1) = 1; // $ uncertain="SSA def(*p)"
+  }
+  use(p); // $ uncertain="SSA phi(*p)"
+  }
+  
+}
+
+void test3(bool b) { // $ certain="SSA def(&b)" certain="SSA def(b)"
+  for(int i = 0; i < 10;) { // $ certain="SSA def(&i)" certain="SSA def(i)" certain="SSA phi(i)"
+    if(b) {
+      ++i; // $ certain="SSA def(i)"
+    }
+    use(i); // $ certain="SSA phi(i)"
+  }
+}
\ No newline at end of file
diff --git a/cpp/ql/test/library-tests/dataflow/certain/test.expected b/cpp/ql/test/library-tests/dataflow/certain/test.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/cpp/ql/test/library-tests/dataflow/certain/test.ql b/cpp/ql/test/library-tests/dataflow/certain/test.ql
new file mode 100644
index 000000000000..231e3c31663e
--- /dev/null
+++ b/cpp/ql/test/library-tests/dataflow/certain/test.ql
@@ -0,0 +1,22 @@
+import cpp
+import utils.test.InlineExpectationsTest
+import semmle.code.cpp.dataflow.new.DataFlow::DataFlow
+
+bindingset[s]
+string quote(string s) { if s.matches("% %") then result = "\"" + s + "\"" else result = s }
+
+module AsDefinitionTest implements TestSig {
+  string getARelevantTag() { result = ["certain", "uncertain"] }
+
+  predicate hasActualResult(Location location, string element, string tag, string value) {
+    exists(Ssa::Definition d |
+      location = d.getLocation() and
+      element = d.toString() and
+      value = quote(d.toString())
+    |
+      if d.isCertain() then tag = "certain" else tag = "uncertain"
+    )
+  }
+}
+
+import MakeTest<AsDefinitionTest>
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected
index f41def013155..3aa5b3c30e02 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected
@@ -65,52 +65,52 @@
 | test.cpp:8:8:8:9 | t1 | test.cpp:9:8:9:9 | t1 |
 | test.cpp:9:8:9:9 | t1 | test.cpp:11:7:11:8 | t1 |
 | test.cpp:9:8:9:9 | t1 | test.cpp:11:7:11:8 | t1 |
-| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | [input] SSA phi read(t2) |
-| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | [input] SSA phi(*t2) |
+| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | [input] SSA phi read(&t2) |
+| test.cpp:10:8:10:9 | t2 | test.cpp:11:7:11:8 | [input] SSA phi(t2) |
 | test.cpp:10:8:10:9 | t2 | test.cpp:13:10:13:11 | t2 |
-| test.cpp:11:7:11:8 | [input] SSA phi read(t2) | test.cpp:15:8:15:9 | t2 |
-| test.cpp:11:7:11:8 | [input] SSA phi(*t2) | test.cpp:15:8:15:9 | t2 |
+| test.cpp:11:7:11:8 | [input] SSA phi read(&t2) | test.cpp:15:8:15:9 | t2 |
+| test.cpp:11:7:11:8 | [input] SSA phi(t2) | test.cpp:15:8:15:9 | t2 |
 | test.cpp:11:7:11:8 | t1 | test.cpp:21:8:21:9 | t1 |
 | test.cpp:12:5:12:10 | ... = ... | test.cpp:13:10:13:11 | t2 |
 | test.cpp:12:10:12:10 | 0 | test.cpp:12:5:12:10 | ... = ... |
 | test.cpp:13:10:13:11 | t2 | test.cpp:15:8:15:9 | t2 |
 | test.cpp:13:10:13:11 | t2 | test.cpp:15:8:15:9 | t2 |
-| test.cpp:15:8:15:9 | t2 | test.cpp:23:15:23:16 | [input] SSA phi read(*t2) |
+| test.cpp:15:8:15:9 | t2 | test.cpp:23:15:23:16 | [input] SSA phi read(&t2) |
 | test.cpp:15:8:15:9 | t2 | test.cpp:23:15:23:16 | [input] SSA phi read(t2) |
 | test.cpp:17:3:17:8 | ... = ... | test.cpp:21:8:21:9 | t1 |
 | test.cpp:17:8:17:8 | 0 | test.cpp:17:3:17:8 | ... = ... |
-| test.cpp:21:8:21:9 | t1 | test.cpp:23:19:23:19 | SSA phi read(t1) |
-| test.cpp:21:8:21:9 | t1 | test.cpp:23:19:23:19 | SSA phi(*t1) |
+| test.cpp:21:8:21:9 | t1 | test.cpp:23:19:23:19 | SSA phi read(&t1) |
+| test.cpp:21:8:21:9 | t1 | test.cpp:23:19:23:19 | SSA phi(t1) |
 | test.cpp:23:15:23:16 | 0 | test.cpp:23:15:23:16 | 0 |
-| test.cpp:23:15:23:16 | 0 | test.cpp:23:19:23:19 | SSA phi(*i) |
-| test.cpp:23:15:23:16 | [input] SSA phi read(*t2) | test.cpp:23:19:23:19 | SSA phi read(*t2) |
+| test.cpp:23:15:23:16 | 0 | test.cpp:23:19:23:19 | SSA phi(i) |
+| test.cpp:23:15:23:16 | [input] SSA phi read(&t2) | test.cpp:23:19:23:19 | SSA phi read(&t2) |
 | test.cpp:23:15:23:16 | [input] SSA phi read(t2) | test.cpp:23:19:23:19 | SSA phi read(t2) |
-| test.cpp:23:19:23:19 | SSA phi read(*t2) | test.cpp:24:10:24:11 | t2 |
-| test.cpp:23:19:23:19 | SSA phi read(i) | test.cpp:23:19:23:19 | i |
-| test.cpp:23:19:23:19 | SSA phi read(t1) | test.cpp:23:23:23:24 | t1 |
+| test.cpp:23:19:23:19 | SSA phi read(&i) | test.cpp:23:19:23:19 | i |
+| test.cpp:23:19:23:19 | SSA phi read(&t1) | test.cpp:23:23:23:24 | t1 |
+| test.cpp:23:19:23:19 | SSA phi read(&t2) | test.cpp:24:10:24:11 | t2 |
 | test.cpp:23:19:23:19 | SSA phi read(t2) | test.cpp:24:10:24:11 | t2 |
-| test.cpp:23:19:23:19 | SSA phi(*i) | test.cpp:23:19:23:19 | i |
-| test.cpp:23:19:23:19 | SSA phi(*t1) | test.cpp:23:23:23:24 | t1 |
+| test.cpp:23:19:23:19 | SSA phi(i) | test.cpp:23:19:23:19 | i |
+| test.cpp:23:19:23:19 | SSA phi(t1) | test.cpp:23:23:23:24 | t1 |
 | test.cpp:23:19:23:19 | i | test.cpp:23:27:23:27 | i |
 | test.cpp:23:19:23:19 | i | test.cpp:23:27:23:27 | i |
-| test.cpp:23:23:23:24 | t1 | test.cpp:23:27:23:29 | [input] SSA phi read(t1) |
+| test.cpp:23:23:23:24 | t1 | test.cpp:23:27:23:29 | [input] SSA phi read(&t1) |
 | test.cpp:23:23:23:24 | t1 | test.cpp:26:8:26:9 | t1 |
 | test.cpp:23:23:23:24 | t1 | test.cpp:26:8:26:9 | t1 |
 | test.cpp:23:27:23:27 | *i | test.cpp:23:27:23:27 | *i |
 | test.cpp:23:27:23:27 | *i | test.cpp:23:27:23:27 | i |
 | test.cpp:23:27:23:27 | i | test.cpp:23:27:23:27 | i |
 | test.cpp:23:27:23:27 | i | test.cpp:23:27:23:27 | i |
-| test.cpp:23:27:23:27 | i | test.cpp:23:27:23:29 | [input] SSA phi read(i) |
+| test.cpp:23:27:23:27 | i | test.cpp:23:27:23:29 | [input] SSA phi read(&i) |
 | test.cpp:23:27:23:29 | ... ++ | test.cpp:23:27:23:29 | ... ++ |
-| test.cpp:23:27:23:29 | ... ++ | test.cpp:23:27:23:29 | [input] SSA phi(*i) |
-| test.cpp:23:27:23:29 | [input] SSA phi read(*t2) | test.cpp:23:19:23:19 | SSA phi read(*t2) |
-| test.cpp:23:27:23:29 | [input] SSA phi read(i) | test.cpp:23:19:23:19 | SSA phi read(i) |
-| test.cpp:23:27:23:29 | [input] SSA phi read(t1) | test.cpp:23:19:23:19 | SSA phi read(t1) |
+| test.cpp:23:27:23:29 | ... ++ | test.cpp:23:27:23:29 | [input] SSA phi(i) |
+| test.cpp:23:27:23:29 | [input] SSA phi read(&i) | test.cpp:23:19:23:19 | SSA phi read(&i) |
+| test.cpp:23:27:23:29 | [input] SSA phi read(&t1) | test.cpp:23:19:23:19 | SSA phi read(&t1) |
+| test.cpp:23:27:23:29 | [input] SSA phi read(&t2) | test.cpp:23:19:23:19 | SSA phi read(&t2) |
 | test.cpp:23:27:23:29 | [input] SSA phi read(t2) | test.cpp:23:19:23:19 | SSA phi read(t2) |
-| test.cpp:23:27:23:29 | [input] SSA phi(*i) | test.cpp:23:19:23:19 | SSA phi(*i) |
-| test.cpp:23:27:23:29 | [input] SSA phi(*t1) | test.cpp:23:19:23:19 | SSA phi(*t1) |
-| test.cpp:24:5:24:11 | ... = ... | test.cpp:23:27:23:29 | [input] SSA phi(*t1) |
-| test.cpp:24:10:24:11 | t2 | test.cpp:23:27:23:29 | [input] SSA phi read(*t2) |
+| test.cpp:23:27:23:29 | [input] SSA phi(i) | test.cpp:23:19:23:19 | SSA phi(i) |
+| test.cpp:23:27:23:29 | [input] SSA phi(t1) | test.cpp:23:19:23:19 | SSA phi(t1) |
+| test.cpp:24:5:24:11 | ... = ... | test.cpp:23:27:23:29 | [input] SSA phi(t1) |
+| test.cpp:24:10:24:11 | t2 | test.cpp:23:27:23:29 | [input] SSA phi read(&t2) |
 | test.cpp:24:10:24:11 | t2 | test.cpp:23:27:23:29 | [input] SSA phi read(t2) |
 | test.cpp:24:10:24:11 | t2 | test.cpp:24:5:24:11 | ... = ... |
 | test.cpp:382:48:382:54 | source1 | test.cpp:384:16:384:23 | *& ... |