From 92a730c9acd6397cfa01db80eef56f72b762df73 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 22 Jul 2025 18:14:21 +0100
Subject: [PATCH 1/8] C++: Add a false positive.

---
 .../CWE-119/SAMATE/OverrunWriteProductFlow.expected   |  6 ++++++
 .../query-tests/Security/CWE/CWE-119/SAMATE/test.cpp  | 11 +++++++++++
 2 files changed, 17 insertions(+)

diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
index 2f24a9a27cb5..e22a736fc7ed 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
@@ -70,6 +70,8 @@ edges
 | test.cpp:262:15:262:30 | call to malloc | test.cpp:266:12:266:12 | p | provenance |  |
 | test.cpp:264:9:264:30 | ... = ... | test.cpp:266:12:266:12 | p | provenance |  |
 | test.cpp:264:13:264:30 | call to malloc | test.cpp:264:9:264:30 | ... = ... | provenance |  |
+| test.cpp:271:14:271:27 | new[] | test.cpp:271:14:271:27 | new[] | provenance |  |
+| test.cpp:271:14:271:27 | new[] | test.cpp:276:12:276:13 | xs | provenance |  |
 nodes
 | test.cpp:16:11:16:21 | **mk_string_t [string] | semmle.label | **mk_string_t [string] |
 | test.cpp:18:5:18:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
@@ -151,6 +153,9 @@ nodes
 | test.cpp:264:9:264:30 | ... = ... | semmle.label | ... = ... |
 | test.cpp:264:13:264:30 | call to malloc | semmle.label | call to malloc |
 | test.cpp:266:12:266:12 | p | semmle.label | p |
+| test.cpp:271:14:271:27 | new[] | semmle.label | new[] |
+| test.cpp:271:14:271:27 | new[] | semmle.label | new[] |
+| test.cpp:276:12:276:13 | xs | semmle.label | xs |
 subpaths
 | test.cpp:242:22:242:27 | buffer | test.cpp:235:40:235:45 | buffer | test.cpp:235:27:235:31 | *p_str [Return] [string] | test.cpp:242:16:242:19 | set_string output argument [string] |
 | test.cpp:242:22:242:27 | buffer | test.cpp:235:40:235:45 | buffer | test.cpp:235:27:235:31 | *p_str [string] | test.cpp:242:16:242:19 | set_string output argument [string] |
@@ -173,3 +178,4 @@ subpaths
 | test.cpp:243:5:243:10 | call to memset | test.cpp:241:20:241:38 | call to malloc | test.cpp:243:12:243:21 | string | This write may overflow $@ by 1 element. | test.cpp:243:16:243:21 | string | string |
 | test.cpp:250:5:250:10 | call to memset | test.cpp:249:14:249:33 | call to my_alloc | test.cpp:250:12:250:12 | p | This write may overflow $@ by 1 element. | test.cpp:250:12:250:12 | p | p |
 | test.cpp:266:5:266:10 | call to memset | test.cpp:262:15:262:30 | call to malloc | test.cpp:266:12:266:12 | p | This write may overflow $@ by 1 element. | test.cpp:266:12:266:12 | p | p |
+| test.cpp:276:5:276:10 | call to memset | test.cpp:271:14:271:27 | new[] | test.cpp:276:12:276:13 | xs | This write may overflow $@ by 1 element. | test.cpp:276:12:276:13 | xs | xs |
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp
index 253ac4fe2925..af1a88f25fbf 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp
@@ -264,4 +264,15 @@ void test7(unsigned n) {
         p = (char*)malloc(++n);
     }
     memset(p, 0, n); // GOOD [FALSE POSITIVE]
+}
+
+void test8(unsigned size, unsigned src_pos)
+{
+  char *xs = new char[size];
+  if (src_pos > size) {
+    src_pos = size;
+  }
+  if (src_pos < size - 1) {
+    memset(xs, 0, src_pos + 1); // GOOD [FALSE POSITIVE]
+  }
 }
\ No newline at end of file

From a1f4246c5fb57703d43eb1e5be6d98aa1cfa0735 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 22 Jul 2025 18:15:10 +0100
Subject: [PATCH 2/8] C++: Extract the barriers from
 'cpp/invalid-pointer-deref' into a library.

---
 .../AllocationToInvalidPointer.qll            | 172 ++----------------
 .../ProductFlowUtils/ProductFlowUtils.qll     | 167 +++++++++++++++++
 2 files changed, 183 insertions(+), 156 deletions(-)
 create mode 100644 cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll

diff --git a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll
index 223d0abf1d4e..2fea5327720a 100644
--- a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll
+++ b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll
@@ -53,44 +53,12 @@
 
 private import cpp
 private import semmle.code.cpp.ir.dataflow.internal.ProductFlow
+private import semmle.code.cpp.security.ProductFlowUtils.ProductFlowUtils
 private import semmle.code.cpp.ir.ValueNumbering
 private import semmle.code.cpp.controlflow.IRGuards
 private import codeql.util.Unit
 private import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
 
-private VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
-
-/**
- * Gets a (sub)expression that may be the result of evaluating `size`.
- *
- * For example, `getASizeCandidate(a ? b : c)` gives `a ? b : c`, `b` and `c`.
- */
-bindingset[size]
-pragma[inline_late]
-private Expr getASizeCandidate(Expr size) {
-  result = size
-  or
-  result = [size.(ConditionalExpr).getThen(), size.(ConditionalExpr).getElse()]
-}
-
-/**
- * Holds if the `(n, state)` pair represents the source of flow for the size
- * expression associated with `alloc`.
- */
-predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
-  exists(VariableAccess va, Expr size, int delta, Expr s |
-    size = alloc.getSizeExpr() and
-    s = getASizeCandidate(size) and
-    // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
-    va = unique( | | getAVariableAccess(s)) and
-    // Compute `delta` as the constant difference between `x` and `x + 1`.
-    bounded1(any(Instruction instr | instr.getUnconvertedResultExpression() = s),
-      any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
-    n.asExpr() = va and
-    state = delta
-  )
-}
-
 /**
  * Gets the virtual dispatch branching limit when calculating field flow while searching
  * for flow from an allocation to the construction of an out-of-bounds pointer.
@@ -100,125 +68,6 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
  */
 int allocationToInvalidPointerFieldFlowBranchLimit() { result = 0 }
 
-/**
- * A module that encapsulates a barrier guard to remove false positives from flow like:
- * ```cpp
- * char *p = new char[size];
- * // ...
- * unsigned n = size;
- * // ...
- * if(n < size) {
- *   use(*p[n]);
- * }
- * ```
- * In this case, the sink pair identified by the product flow library (without any additional barriers)
- * would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
- * instruction `pai = a + b` such that:
- * 1. the allocation flows to `a`, and
- * 2. `b <= n` where `n` is the `n` in `p[n]`
- * but because there's a strict comparison that compares `n` against the size of the allocation this
- * snippet is fine.
- */
-private module SizeBarrier {
-  private module SizeBarrierConfig implements DataFlow::ConfigSig {
-    predicate isSource(DataFlow::Node source) {
-      // The sources is the same as in the sources for the second
-      // projection in the `AllocToInvalidPointerConfig` module.
-      hasSize(_, source, _) and
-      InterestingPointerAddInstruction::isInterestingSize(source)
-    }
-
-    int fieldFlowBranchLimit() { result = allocationToInvalidPointerFieldFlowBranchLimit() }
-
-    /**
-     * Holds if `small <= large + k` holds if `g` evaluates to `testIsTrue`.
-     */
-    additional predicate isSink(
-      DataFlow::Node small, DataFlow::Node large, IRGuardCondition g, int k, boolean testIsTrue
-    ) {
-      // The sink is any "large" side of a relational comparison. i.e., the `large` expression
-      // in a guard such as `small <= large + k`.
-      g.comparesLt(small.asOperand(), large.asOperand(), k + 1, true, testIsTrue)
-    }
-
-    predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
-  }
-
-  module SizeBarrierFlow = DataFlow::Global<SizeBarrierConfig>;
-
-  private int getASizeAddend(DataFlow::Node node) {
-    exists(DataFlow::Node source |
-      SizeBarrierFlow::flow(source, node) and
-      hasSize(_, source, result)
-    )
-  }
-
-  /**
-   * Holds if `small <= large + k` holds if `g` evaluates to `edge`.
-   */
-  private predicate operandGuardChecks(
-    IRGuardCondition g, Operand small, DataFlow::Node large, int k, boolean edge
-  ) {
-    SizeBarrierFlow::flowTo(large) and
-    SizeBarrierConfig::isSink(DataFlow::operandNode(small), large, g, k, edge)
-  }
-
-  /**
-   * Gets an instruction `instr` that is guarded by a check such as `instr <= small + delta` where
-   * `small <= _ + k` and `small` is the "small side" of of a relational comparison that checks
-   * whether `small <= size` where `size` is the size of an allocation.
-   */
-  Instruction getABarrierInstruction0(int delta, int k) {
-    exists(
-      IRGuardCondition g, ValueNumber value, Operand small, boolean edge, DataFlow::Node large
-    |
-      // We know:
-      // 1. result <= value + delta (by `bounded`)
-      // 2. value <= large + k (by `operandGuardChecks`).
-      // So:
-      // result <= value + delta (by 1.)
-      //        <= large + k + delta (by 2.)
-      small = value.getAUse() and
-      operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](small), large,
-        pragma[only_bind_into](k), pragma[only_bind_into](edge)) and
-      bounded(result, value.getAnInstruction(), delta) and
-      g.controls(result.getBlock(), edge) and
-      k < getASizeAddend(large)
-    )
-  }
-
-  /**
-   * Gets an instruction that is guarded by a guard condition which ensures that
-   * the value of the instruction is upper-bounded by size of some allocation.
-   */
-  bindingset[state]
-  pragma[inline_late]
-  Instruction getABarrierInstruction(int state) {
-    exists(int delta, int k |
-      state > k + delta and
-      // result <= "size of allocation" + delta + k
-      //        < "size of allocation" + state
-      result = getABarrierInstruction0(delta, k)
-    )
-  }
-
-  /**
-   * Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
-   * the value of the node is upper-bounded by size of some allocation.
-   */
-  DataFlow::Node getABarrierNode(int state) {
-    exists(DataFlow::Node source, int delta, int k |
-      SizeBarrierFlow::flow(source, result) and
-      hasSize(_, source, state) and
-      result.asInstruction() = SizeBarrier::getABarrierInstruction0(delta, k) and
-      state > k + delta
-      // so now we have:
-      // result <= "size of allocation" + delta + k
-      //        < "size of allocation" + state
-    )
-  }
-}
-
 private module InterestingPointerAddInstruction {
   private module PointerAddInstructionConfig implements DataFlow::ConfigSig {
     predicate isSource(DataFlow::Node source) {
@@ -227,7 +76,7 @@ private module InterestingPointerAddInstruction {
       hasSize(source.asExpr(), _, _)
     }
 
-    int fieldFlowBranchLimit() { result = allocationToInvalidPointerFieldFlowBranchLimit() }
+    predicate fieldFlowBranchLimit = allocationToInvalidPointerFieldFlowBranchLimit/0;
 
     predicate isSink(DataFlow::Node sink) {
       sink.asInstruction() = any(PointerAddInstruction pai).getLeft()
@@ -263,6 +112,17 @@ private module InterestingPointerAddInstruction {
   }
 }
 
+private module SizeBarrierInput implements SizeBarrierInputSig {
+  predicate fieldFlowBranchLimit = allocationToInvalidPointerFieldFlowBranchLimit/0;
+
+  predicate isSource(DataFlow::Node source) {
+    // The sources is the same as in the sources for the second
+    // projection in the `AllocToInvalidPointerConfig` module.
+    hasSize(_, source, _) and
+    InterestingPointerAddInstruction::isInterestingSize(source)
+  }
+}
+
 /**
  * A product-flow configuration for flow from an `(allocation, size)` pair to a
  * pointer-arithmetic operation `pai` such that `pai <= allocation + size`.
@@ -301,7 +161,7 @@ private module Config implements ProductFlow::StateConfigSig {
   private import semmle.code.cpp.ir.dataflow.internal.DataFlowPrivate
 
   predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
-    node = SizeBarrier::getABarrierNode(state)
+    node = SizeBarrier<SizeBarrierInput>::getABarrierNode(state)
   }
 
   predicate isBarrier2(DataFlow::Node node) {
@@ -357,8 +217,8 @@ private predicate pointerAddInstructionHasBounds0(
     sizeInstr = sizeSink.asInstruction() and
     // pai.getRight() <= sizeSink + delta
     bounded1(right, sizeInstr, delta) and
-    not right = SizeBarrier::getABarrierInstruction(delta) and
-    not sizeInstr = SizeBarrier::getABarrierInstruction(delta)
+    not right = SizeBarrier<SizeBarrierInput>::getABarrierInstruction(delta) and
+    not sizeInstr = SizeBarrier<SizeBarrierInput>::getABarrierInstruction(delta)
   )
 }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll b/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
new file mode 100644
index 000000000000..e7275bc57e2b
--- /dev/null
+++ b/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
@@ -0,0 +1,167 @@
+/**
+ * This file provies the `SizeBarrier` module which provides barriers for
+ * both the `cpp/invalid-pointer-deref` query and the `cpp/overrun-write`
+ * query.
+ */
+
+private import cpp
+private import semmle.code.cpp.dataflow.new.DataFlow
+private import semmle.code.cpp.ir.ValueNumbering
+private import semmle.code.cpp.controlflow.IRGuards
+private import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
+
+private VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
+
+/**
+ * Gets a (sub)expression that may be the result of evaluating `size`.
+ *
+ * For example, `getASizeCandidate(a ? b : c)` gives `a ? b : c`, `b` and `c`.
+ */
+bindingset[size]
+pragma[inline_late]
+private Expr getASizeCandidate(Expr size) {
+  result = size
+  or
+  result = [size.(ConditionalExpr).getThen(), size.(ConditionalExpr).getElse()]
+}
+
+/**
+ * Holds if the `(n, state)` pair represents the source of flow for the size
+ * expression associated with `alloc`.
+ */
+predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
+  exists(VariableAccess va, Expr size, int delta, Expr s |
+    size = alloc.getSizeExpr() and
+    s = getASizeCandidate(size) and
+    // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
+    va = unique( | | getAVariableAccess(s)) and
+    // Compute `delta` as the constant difference between `x` and `x + 1`.
+    bounded1(any(Instruction instr | instr.getUnconvertedResultExpression() = s),
+      any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
+    n.asExpr() = va and
+    state = delta
+  )
+}
+
+/** Provides the input specification of the `SizeBarrier` module. */
+signature module SizeBarrierInputSig {
+  /** Gets the virtual dispatch branching limit when calculating field flow. */
+  int fieldFlowBranchLimit();
+
+  /** Holds if `source` is a relevant data flow source. */
+  predicate isSource(DataFlow::Node source);
+}
+
+/**
+ * A module that encapsulates a barrier guard to remove false positives from flow like:
+ * ```cpp
+ * char *p = new char[size];
+ * // ...
+ * unsigned n = size;
+ * // ...
+ * if(n < size) {
+ *   use(*p[n]);
+ * }
+ * ```
+ * In this case, the sink pair identified by the product flow library (without any additional barriers)
+ * would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
+ * instruction `pai = a + b` such that:
+ * 1. the allocation flows to `a`, and
+ * 2. `b <= n` where `n` is the `n` in `p[n]`
+ * but because there's a strict comparison that compares `n` against the size of the allocation this
+ * snippet is fine.
+ */
+module SizeBarrier<SizeBarrierInputSig Input> {
+  private module SizeBarrierConfig implements DataFlow::ConfigSig {
+    predicate isSource = Input::isSource/1;
+
+    predicate fieldFlowBranchLimit = Input::fieldFlowBranchLimit/0;
+
+    /**
+     * Holds if `small <= large + k` holds if `g` evaluates to `testIsTrue`.
+     */
+    additional predicate isSink(
+      DataFlow::Node small, DataFlow::Node large, IRGuardCondition g, int k, boolean testIsTrue
+    ) {
+      // The sink is any "large" side of a relational comparison. i.e., the `large` expression
+      // in a guard such as `small <= large + k`.
+      g.comparesLt(small.asOperand(), large.asOperand(), k + 1, true, testIsTrue)
+    }
+
+    predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
+  }
+
+  private module SizeBarrierFlow = DataFlow::Global<SizeBarrierConfig>;
+
+  private int getASizeAddend(DataFlow::Node node) {
+    exists(DataFlow::Node source |
+      SizeBarrierFlow::flow(source, node) and
+      hasSize(_, source, result)
+    )
+  }
+
+  /**
+   * Holds if `small <= large + k` holds if `g` evaluates to `edge`.
+   */
+  private predicate operandGuardChecks(
+    IRGuardCondition g, Operand small, DataFlow::Node large, int k, boolean edge
+  ) {
+    SizeBarrierFlow::flowTo(large) and
+    SizeBarrierConfig::isSink(DataFlow::operandNode(small), large, g, k, edge)
+  }
+
+  /**
+   * Gets an instruction `instr` that is guarded by a check such as `instr <= small + delta` where
+   * `small <= _ + k` and `small` is the "small side" of of a relational comparison that checks
+   * whether `small <= size` where `size` is the size of an allocation.
+   */
+  private Instruction getABarrierInstruction0(int delta, int k) {
+    exists(
+      IRGuardCondition g, ValueNumber value, Operand small, boolean edge, DataFlow::Node large
+    |
+      // We know:
+      // 1. result <= value + delta (by `bounded`)
+      // 2. value <= large + k (by `operandGuardChecks`).
+      // So:
+      // result <= value + delta (by 1.)
+      //        <= large + k + delta (by 2.)
+      small = value.getAUse() and
+      operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](small), large,
+        pragma[only_bind_into](k), pragma[only_bind_into](edge)) and
+      bounded(result, value.getAnInstruction(), delta) and
+      g.controls(result.getBlock(), edge) and
+      k < getASizeAddend(large)
+    )
+  }
+
+  /**
+   * Gets an instruction that is guarded by a guard condition which ensures that
+   * the value of the instruction is upper-bounded by size of some allocation.
+   */
+  bindingset[state]
+  pragma[inline_late]
+  Instruction getABarrierInstruction(int state) {
+    exists(int delta, int k |
+      state > k + delta and
+      // result <= "size of allocation" + delta + k
+      //        < "size of allocation" + state
+      result = getABarrierInstruction0(delta, k)
+    )
+  }
+
+  /**
+   * Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
+   * the value of the node is upper-bounded by size of some allocation.
+   */
+  DataFlow::Node getABarrierNode(int state) {
+    exists(DataFlow::Node source, int delta, int k |
+      SizeBarrierFlow::flow(source, result) and
+      hasSize(_, source, state) and
+      result.asInstruction() = getABarrierInstruction0(delta, k) and
+      state > k + delta
+      // so now we have:
+      // result <= "size of allocation" + delta + k
+      //        < "size of allocation" + state
+    )
+  }
+}

From e0eadc75dde8b42002233ed4a8a53420ad60e46f Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 22 Jul 2025 18:21:51 +0100
Subject: [PATCH 3/8] C++: Remove the ad-hoc code for keeping track of
 increments/decrements on pointers in the 'cpp/overrun-write' query.

---
 .../CWE/CWE-119/OverrunWriteProductFlow.ql    | 85 +------------------
 .../SAMATE/OverrunWriteProductFlow.expected   | 49 -----------
 2 files changed, 4 insertions(+), 130 deletions(-)

diff --git a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
index b193b846b5a8..ffe645287580 100644
--- a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
+++ b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
@@ -88,81 +88,14 @@ module ValidState {
 
     predicate isSink(DataFlow::Node sink) { isSinkPairImpl(_, _, sink, _, _) }
 
-    predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
-      isAdditionalFlowStep2(node1, node2, _)
-    }
-
-    predicate includeHiddenNodes() { any() }
+    predicate isBarrierOut(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
   }
 
   private import DataFlow::Global<ValidStateConfig>
 
-  private predicate inLoop(PathNode n) { n.getASuccessor+() = n }
-
-  /**
-   * Holds if `value` is a possible offset for `n`.
-   *
-   * To ensure termination, we limit `value` to be in the
-   * range `[-2, 2]` if the node is part of a loop. Without
-   * this restriction we wouldn't terminate on an example like:
-   * ```cpp
-   * while(unknown()) { size++; }
-   * ```
-   */
-  private predicate validStateImpl(PathNode n, int value) {
-    // If the dataflow node depends recursively on itself we restrict the range.
-    (inLoop(n) implies value = [-2 .. 2]) and
-    (
-      // For the dataflow source we have an allocation such as `malloc(size + k)`,
-      // and the value of the flow-state is then `k`.
-      hasSize(_, n.getNode(), value)
-      or
-      // For a dataflow sink any `value` that is strictly smaller than the delta
-      // needs to be a valid flow-state. That is, for a snippet like:
-      // ```
-      // p = b ? new char[size] : new char[size + 1];
-      // memset(p, 0, size + 2);
-      // ```
-      // the valid flow-states at the `memset` must include the set `{0, 1}` since the
-      // flow-state at `new char[size]` is `0`, and the flow-state at `new char[size + 1]`
-      // is `1`.
-      //
-      // So we find a valid flow-state at the sink's predecessor, and use the definition
-      // of our sink predicate to compute the valid flow-states at the sink.
-      exists(int delta, PathNode n0 |
-        n0.getASuccessor() = n and
-        validStateImpl(n0, value) and
-        isSinkPairImpl(_, _, n.getNode(), delta, _) and
-        delta > value
-      )
-      or
-      // For a non-source and non-sink node there is two cases to consider.
-      // 1. A node where we have to update the flow-state, or
-      // 2. A node that doesn't update the flow-state.
-      //
-      // For case 1, we compute the new flow-state by adding the constant operand of the
-      // `AddInstruction` to the flow-state of any predecessor node.
-      // For case 2 we simply propagate the valid flow-states from the predecessor node to
-      // the next one.
-      exists(PathNode n0, DataFlow::Node node0, DataFlow::Node node, int value0 |
-        n0.getASuccessor() = n and
-        validStateImpl(n0, value0) and
-        node = n.getNode() and
-        node0 = n0.getNode()
-      |
-        exists(int delta |
-          isAdditionalFlowStep2(node0, node, delta) and
-          value0 = value + delta
-        )
-        or
-        not isAdditionalFlowStep2(node0, node, _) and
-        value = value0
-      )
-    )
-  }
-
-  predicate validState(DataFlow::Node n, int value) {
-    validStateImpl(any(PathNode pn | pn.getNode() = n), value)
+  predicate validState(DataFlow::Node source, DataFlow::Node sink, int value) {
+    hasSize(_, source, value) and
+    flow(source, sink)
   }
 }
 
@@ -213,16 +146,6 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
   }
 
   predicate isBarrierOut2(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
-
-  predicate isAdditionalFlowStep2(
-    DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
-  ) {
-    validState(node2, state2) and
-    exists(int delta |
-      isAdditionalFlowStep2(node1, node2, delta) and
-      state1 = state2 + delta
-    )
-  }
 }
 
 module StringSizeFlow = ProductFlow::GlobalWithState<StringSizeConfig>;
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
index e22a736fc7ed..b0a61f6ab630 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
@@ -12,19 +12,6 @@ edges
 | test.cpp:42:13:42:15 | *str [string] | test.cpp:42:18:42:23 | string | provenance |  |
 | test.cpp:72:17:72:19 | *str [string] | test.cpp:72:22:72:27 | string | provenance |  |
 | test.cpp:80:17:80:19 | *str [string] | test.cpp:80:22:80:27 | string | provenance |  |
-| test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | provenance |  |
-| test.cpp:90:5:90:7 | *str [post update] [string] | test.cpp:91:5:91:7 | *str [string] | provenance |  |
-| test.cpp:90:5:90:34 | ... = ... | test.cpp:90:5:90:7 | *str [post update] [string] | provenance |  |
-| test.cpp:90:19:90:24 | call to malloc | test.cpp:90:5:90:34 | ... = ... | provenance |  |
-| test.cpp:91:5:91:7 | *str [string] | test.cpp:92:12:92:14 | *str [string] | provenance |  |
-| test.cpp:92:12:92:14 | *str [string] | test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:99:13:99:15 | *str [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:129:17:129:19 | *str [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:137:17:137:19 | *str [string] | provenance |  |
-| test.cpp:99:13:99:15 | *str [string] | test.cpp:99:18:99:23 | string | provenance |  |
-| test.cpp:129:17:129:19 | *str [string] | test.cpp:129:22:129:27 | string | provenance |  |
-| test.cpp:137:17:137:19 | *str [string] | test.cpp:137:22:137:27 | string | provenance |  |
 | test.cpp:147:5:147:7 | *str [post update] [string] | test.cpp:148:5:148:7 | *str [string] | provenance |  |
 | test.cpp:147:5:147:34 | ... = ... | test.cpp:147:5:147:7 | *str [post update] [string] | provenance |  |
 | test.cpp:147:19:147:24 | call to malloc | test.cpp:147:5:147:34 | ... = ... | provenance |  |
@@ -46,12 +33,6 @@ edges
 | test.cpp:199:17:199:19 | *str [string] | test.cpp:199:22:199:27 | string | provenance |  |
 | test.cpp:203:17:203:19 | *str [string] | test.cpp:203:22:203:27 | string | provenance |  |
 | test.cpp:207:17:207:19 | *str [string] | test.cpp:207:22:207:27 | string | provenance |  |
-| test.cpp:214:24:214:24 | p | test.cpp:216:10:216:10 | p | provenance |  |
-| test.cpp:220:27:220:54 | call to malloc | test.cpp:220:27:220:54 | call to malloc | provenance |  |
-| test.cpp:220:27:220:54 | call to malloc | test.cpp:222:15:222:20 | buffer | provenance |  |
-| test.cpp:222:15:222:20 | buffer | test.cpp:214:24:214:24 | p | provenance |  |
-| test.cpp:228:27:228:54 | call to malloc | test.cpp:228:27:228:54 | call to malloc | provenance |  |
-| test.cpp:228:27:228:54 | call to malloc | test.cpp:232:10:232:15 | buffer | provenance |  |
 | test.cpp:235:40:235:45 | buffer | test.cpp:236:5:236:26 | ... = ... | provenance |  |
 | test.cpp:236:5:236:9 | *p_str [post update] [string] | test.cpp:235:27:235:31 | *p_str [Return] [string] | provenance |  |
 | test.cpp:236:5:236:9 | *p_str [post update] [string] | test.cpp:235:27:235:31 | *p_str [string] | provenance |  |
@@ -64,8 +45,6 @@ edges
 | test.cpp:243:12:243:14 | *str [string] | test.cpp:243:12:243:21 | string | provenance |  |
 | test.cpp:249:14:249:33 | call to my_alloc | test.cpp:249:14:249:33 | call to my_alloc | provenance |  |
 | test.cpp:249:14:249:33 | call to my_alloc | test.cpp:250:12:250:12 | p | provenance |  |
-| test.cpp:256:5:256:25 | ... = ... | test.cpp:257:12:257:12 | p | provenance |  |
-| test.cpp:256:9:256:25 | call to malloc | test.cpp:256:5:256:25 | ... = ... | provenance |  |
 | test.cpp:262:15:262:30 | call to malloc | test.cpp:262:15:262:30 | call to malloc | provenance |  |
 | test.cpp:262:15:262:30 | call to malloc | test.cpp:266:12:266:12 | p | provenance |  |
 | test.cpp:264:9:264:30 | ... = ... | test.cpp:266:12:266:12 | p | provenance |  |
@@ -87,20 +66,6 @@ nodes
 | test.cpp:72:22:72:27 | string | semmle.label | string |
 | test.cpp:80:17:80:19 | *str [string] | semmle.label | *str [string] |
 | test.cpp:80:22:80:27 | string | semmle.label | string |
-| test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | semmle.label | **mk_string_t_plus_one [string] |
-| test.cpp:90:5:90:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
-| test.cpp:90:5:90:34 | ... = ... | semmle.label | ... = ... |
-| test.cpp:90:19:90:24 | call to malloc | semmle.label | call to malloc |
-| test.cpp:91:5:91:7 | *str [string] | semmle.label | *str [string] |
-| test.cpp:92:12:92:14 | *str [string] | semmle.label | *str [string] |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | semmle.label | *call to mk_string_t_plus_one [string] |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | semmle.label | *call to mk_string_t_plus_one [string] |
-| test.cpp:99:13:99:15 | *str [string] | semmle.label | *str [string] |
-| test.cpp:99:18:99:23 | string | semmle.label | string |
-| test.cpp:129:17:129:19 | *str [string] | semmle.label | *str [string] |
-| test.cpp:129:22:129:27 | string | semmle.label | string |
-| test.cpp:137:17:137:19 | *str [string] | semmle.label | *str [string] |
-| test.cpp:137:22:137:27 | string | semmle.label | string |
 | test.cpp:147:5:147:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
 | test.cpp:147:5:147:34 | ... = ... | semmle.label | ... = ... |
 | test.cpp:147:19:147:24 | call to malloc | semmle.label | call to malloc |
@@ -123,14 +88,6 @@ nodes
 | test.cpp:203:22:203:27 | string | semmle.label | string |
 | test.cpp:207:17:207:19 | *str [string] | semmle.label | *str [string] |
 | test.cpp:207:22:207:27 | string | semmle.label | string |
-| test.cpp:214:24:214:24 | p | semmle.label | p |
-| test.cpp:216:10:216:10 | p | semmle.label | p |
-| test.cpp:220:27:220:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:220:27:220:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:222:15:222:20 | buffer | semmle.label | buffer |
-| test.cpp:228:27:228:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:228:27:228:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:232:10:232:15 | buffer | semmle.label | buffer |
 | test.cpp:235:27:235:31 | *p_str [Return] [string] | semmle.label | *p_str [Return] [string] |
 | test.cpp:235:27:235:31 | *p_str [string] | semmle.label | *p_str [string] |
 | test.cpp:235:40:235:45 | buffer | semmle.label | buffer |
@@ -145,9 +102,6 @@ nodes
 | test.cpp:249:14:249:33 | call to my_alloc | semmle.label | call to my_alloc |
 | test.cpp:249:14:249:33 | call to my_alloc | semmle.label | call to my_alloc |
 | test.cpp:250:12:250:12 | p | semmle.label | p |
-| test.cpp:256:5:256:25 | ... = ... | semmle.label | ... = ... |
-| test.cpp:256:9:256:25 | call to malloc | semmle.label | call to malloc |
-| test.cpp:257:12:257:12 | p | semmle.label | p |
 | test.cpp:262:15:262:30 | call to malloc | semmle.label | call to malloc |
 | test.cpp:262:15:262:30 | call to malloc | semmle.label | call to malloc |
 | test.cpp:264:9:264:30 | ... = ... | semmle.label | ... = ... |
@@ -163,9 +117,6 @@ subpaths
 | test.cpp:42:5:42:11 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:42:18:42:23 | string | This write may overflow $@ by 1 element. | test.cpp:42:18:42:23 | string | string |
 | test.cpp:72:9:72:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:72:22:72:27 | string | This write may overflow $@ by 1 element. | test.cpp:72:22:72:27 | string | string |
 | test.cpp:80:9:80:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:80:22:80:27 | string | This write may overflow $@ by 2 elements. | test.cpp:80:22:80:27 | string | string |
-| test.cpp:99:5:99:11 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:99:18:99:23 | string | This write may overflow $@ by 1 element. | test.cpp:99:18:99:23 | string | string |
-| test.cpp:129:9:129:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:129:22:129:27 | string | This write may overflow $@ by 1 element. | test.cpp:129:22:129:27 | string | string |
-| test.cpp:137:9:137:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:137:22:137:27 | string | This write may overflow $@ by 2 elements. | test.cpp:137:22:137:27 | string | string |
 | test.cpp:152:5:152:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:152:18:152:23 | string | This write may overflow $@ by 1 element. | test.cpp:152:18:152:23 | string | string |
 | test.cpp:154:5:154:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:154:18:154:23 | string | This write may overflow $@ by 1 element. | test.cpp:154:18:154:23 | string | string |
 | test.cpp:156:5:156:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:156:18:156:23 | string | This write may overflow $@ by 2 elements. | test.cpp:156:18:156:23 | string | string |

From a502bb1ac21c510d5d8e18592a42155307d79ad2 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 22 Jul 2025 18:35:50 +0100
Subject: [PATCH 4/8] C++: Add a copy of 'isSinkPairImpl' (named
 'isSinkPairImpl0') with a few more columns that we'll need.

---
 .../CWE/CWE-119/OverrunWriteProductFlow.ql    | 28 ++++++++++++-------
 1 file changed, 18 insertions(+), 10 deletions(-)

diff --git a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
index ffe645287580..95fb01724283 100644
--- a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
+++ b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
@@ -43,20 +43,28 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
   )
 }
 
-predicate isSinkPairImpl(
-  CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf
+/**
+ * Holds if `c` a call to an `ArrayFunction` with buffer argument `bufSink`,
+ * and a size argument `sizeInstr` which satisfies `sizeInstr <= sizeBound + delta`.
+ *
+ * Furthermore, the `sizeSink` node is the dataflow node corresponding to
+ * `sizeBound`, and the expression `eBuf` is the expression corresponding
+ * to `bufInstr`.
+ */
+predicate isSinkPairImpl0(
+  CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf,
+  Instruction sizeBound, Instruction sizeInstr
 ) {
-  exists(
-    int bufIndex, int sizeIndex, Instruction sizeInstr, Instruction bufInstr, ArrayFunction func
-  |
+  exists(int bufIndex, int sizeIndex, Instruction bufInstr, ArrayFunction func |
     bufInstr = bufSink.asInstruction() and
     c.getArgument(bufIndex) = bufInstr and
-    sizeInstr = sizeSink.asInstruction() and
+    sizeBound = sizeSink.asInstruction() and
+    c.getArgument(sizeIndex) = sizeInstr and
     c.getStaticCallTarget() = func and
     pragma[only_bind_into](func)
         .hasArrayWithVariableSize(pragma[only_bind_into](bufIndex),
           pragma[only_bind_into](sizeIndex)) and
-    bounded(c.getArgument(sizeIndex), sizeInstr, delta) and
+    bounded(sizeInstr, sizeBound, delta) and
     eBuf = bufInstr.getUnconvertedResultExpression()
   )
 }
@@ -86,7 +94,7 @@ module ValidState {
   private module ValidStateConfig implements DataFlow::ConfigSig {
     predicate isSource(DataFlow::Node source) { hasSize(_, source, _) }
 
-    predicate isSink(DataFlow::Node sink) { isSinkPairImpl(_, _, sink, _, _) }
+    predicate isSink(DataFlow::Node sink) { isSinkPairImpl0(_, _, sink, _, _, _, _) }
 
     predicate isBarrierOut(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
   }
@@ -131,14 +139,14 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
     // to the size of the allocation. This state is then checked in `isSinkPair`.
     exists(state1) and
     hasSize(bufSource.asExpr(), sizeSource, state2) and
-    validState(sizeSource, state2)
+    validState(sizeSource, _, state2)
   }
 
   predicate isSinkPair(
     DataFlow::Node bufSink, FlowState1 state1, DataFlow::Node sizeSink, FlowState2 state2
   ) {
     exists(state1) and
-    validState(sizeSink, state2) and
+    validState(_, sizeSink, state2) and
     exists(int delta |
       isSinkPairImpl(_, bufSink, sizeSink, delta, _) and
       delta > state2

From 1189665970acc1645fc349a7e5d6f42c1c193e30 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 22 Jul 2025 18:32:18 +0100
Subject: [PATCH 5/8] C++: Add barriers to 'cpp/overrun-write'.

---
 .../CWE/CWE-119/OverrunWriteProductFlow.ql    | 34 +++++++++++++------
 .../SAMATE/OverrunWriteProductFlow.expected   |  6 ----
 .../Security/CWE/CWE-119/SAMATE/test.cpp      |  2 +-
 3 files changed, 24 insertions(+), 18 deletions(-)

diff --git a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
index 95fb01724283..c2ebb4879a99 100644
--- a/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
+++ b/cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql
@@ -20,6 +20,7 @@ import semmle.code.cpp.models.interfaces.Allocation
 import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
+import semmle.code.cpp.security.ProductFlowUtils.ProductFlowUtils
 import semmle.code.cpp.rangeanalysis.new.RangeAnalysisUtil
 import StringSizeFlow::PathGraph1
 import codeql.util.Unit
@@ -109,17 +110,24 @@ module ValidState {
 
 import ValidState
 
-/**
- * Holds if `node2` is a dataflow node that represents an addition of two operands `op1`
- * and `op2` such that:
- * 1. `node1` is the dataflow node that represents `op1`, and
- * 2. the value of `op2` can be upper bounded by `delta.`
- */
-predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2, int delta) {
-  exists(AddInstruction add, Operand op |
-    add.hasOperands(node1.asOperand(), op) and
-    semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
-    node2.asInstruction() = add
+module SizeBarrierInput implements SizeBarrierInputSig {
+  int fieldFlowBranchLimit() { result = 2 }
+
+  predicate isSource(DataFlow::Node source) {
+    exists(int state |
+      hasSize(_, source, state) and
+      validState(source, _, state)
+    )
+  }
+}
+
+predicate isSinkPairImpl(
+  CallInstruction c, DataFlow::Node bufSink, DataFlow::Node sizeSink, int delta, Expr eBuf
+) {
+  exists(Instruction sizeBound, Instruction sizeInstr |
+    isSinkPairImpl0(c, bufSink, sizeSink, delta, eBuf, sizeBound, sizeInstr) and
+    not sizeBound = SizeBarrier<SizeBarrierInput>::getABarrierInstruction(delta) and
+    not sizeInstr = SizeBarrier<SizeBarrierInput>::getABarrierInstruction(delta)
   )
 }
 
@@ -154,6 +162,10 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
   }
 
   predicate isBarrierOut2(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
+
+  predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
+    node = SizeBarrier<SizeBarrierInput>::getABarrierNode(state)
+  }
 }
 
 module StringSizeFlow = ProductFlow::GlobalWithState<StringSizeConfig>;
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
index b0a61f6ab630..3a2b7372831d 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected
@@ -49,8 +49,6 @@ edges
 | test.cpp:262:15:262:30 | call to malloc | test.cpp:266:12:266:12 | p | provenance |  |
 | test.cpp:264:9:264:30 | ... = ... | test.cpp:266:12:266:12 | p | provenance |  |
 | test.cpp:264:13:264:30 | call to malloc | test.cpp:264:9:264:30 | ... = ... | provenance |  |
-| test.cpp:271:14:271:27 | new[] | test.cpp:271:14:271:27 | new[] | provenance |  |
-| test.cpp:271:14:271:27 | new[] | test.cpp:276:12:276:13 | xs | provenance |  |
 nodes
 | test.cpp:16:11:16:21 | **mk_string_t [string] | semmle.label | **mk_string_t [string] |
 | test.cpp:18:5:18:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
@@ -107,9 +105,6 @@ nodes
 | test.cpp:264:9:264:30 | ... = ... | semmle.label | ... = ... |
 | test.cpp:264:13:264:30 | call to malloc | semmle.label | call to malloc |
 | test.cpp:266:12:266:12 | p | semmle.label | p |
-| test.cpp:271:14:271:27 | new[] | semmle.label | new[] |
-| test.cpp:271:14:271:27 | new[] | semmle.label | new[] |
-| test.cpp:276:12:276:13 | xs | semmle.label | xs |
 subpaths
 | test.cpp:242:22:242:27 | buffer | test.cpp:235:40:235:45 | buffer | test.cpp:235:27:235:31 | *p_str [Return] [string] | test.cpp:242:16:242:19 | set_string output argument [string] |
 | test.cpp:242:22:242:27 | buffer | test.cpp:235:40:235:45 | buffer | test.cpp:235:27:235:31 | *p_str [string] | test.cpp:242:16:242:19 | set_string output argument [string] |
@@ -129,4 +124,3 @@ subpaths
 | test.cpp:243:5:243:10 | call to memset | test.cpp:241:20:241:38 | call to malloc | test.cpp:243:12:243:21 | string | This write may overflow $@ by 1 element. | test.cpp:243:16:243:21 | string | string |
 | test.cpp:250:5:250:10 | call to memset | test.cpp:249:14:249:33 | call to my_alloc | test.cpp:250:12:250:12 | p | This write may overflow $@ by 1 element. | test.cpp:250:12:250:12 | p | p |
 | test.cpp:266:5:266:10 | call to memset | test.cpp:262:15:262:30 | call to malloc | test.cpp:266:12:266:12 | p | This write may overflow $@ by 1 element. | test.cpp:266:12:266:12 | p | p |
-| test.cpp:276:5:276:10 | call to memset | test.cpp:271:14:271:27 | new[] | test.cpp:276:12:276:13 | xs | This write may overflow $@ by 1 element. | test.cpp:276:12:276:13 | xs | xs |
diff --git a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp
index af1a88f25fbf..ca6ca9a5c5a8 100644
--- a/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp
+++ b/cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/test.cpp
@@ -273,6 +273,6 @@ void test8(unsigned size, unsigned src_pos)
     src_pos = size;
   }
   if (src_pos < size - 1) {
-    memset(xs, 0, src_pos + 1); // GOOD [FALSE POSITIVE]
+    memset(xs, 0, src_pos + 1); // GOOD
   }
 }
\ No newline at end of file

From 019447b6815881fffb2c30d6b295e6c3372526b7 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Wed, 23 Jul 2025 11:49:07 +0100
Subject: [PATCH 6/8] C++: Add change note.

---
 cpp/ql/lib/change-notes/2025-07-23-overrun-write.md | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 cpp/ql/lib/change-notes/2025-07-23-overrun-write.md

diff --git a/cpp/ql/lib/change-notes/2025-07-23-overrun-write.md b/cpp/ql/lib/change-notes/2025-07-23-overrun-write.md
new file mode 100644
index 000000000000..e221854c49f7
--- /dev/null
+++ b/cpp/ql/lib/change-notes/2025-07-23-overrun-write.md
@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The `cpp/overrun-write` query now recognizes more bound checks and thus produces fewer false positives.
\ No newline at end of file

From 5d6c4a63bb6fc648fe4bf9ceffdbe20d9e65288c Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Wed, 23 Jul 2025 11:53:55 +0100
Subject: [PATCH 7/8] Update
 cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
---
 .../code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll b/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
index e7275bc57e2b..435e8c27e84f 100644
--- a/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
@@ -1,5 +1,5 @@
 /**
- * This file provies the `SizeBarrier` module which provides barriers for
+ * This file provides the `SizeBarrier` module which provides barriers for
  * both the `cpp/invalid-pointer-deref` query and the `cpp/overrun-write`
  * query.
  */

From 3a977b86d46e26077cc435428feff3df4fe66da6 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Wed, 23 Jul 2025 12:27:38 +0100
Subject: [PATCH 8/8] Update
 cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll

Co-authored-by: Idriss Riouak <idrissrio@github.com>
---
 .../code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll b/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
index 435e8c27e84f..151c5d1ae22a 100644
--- a/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/security/ProductFlowUtils/ProductFlowUtils.qll
@@ -112,7 +112,7 @@ module SizeBarrier<SizeBarrierInputSig Input> {
 
   /**
    * Gets an instruction `instr` that is guarded by a check such as `instr <= small + delta` where
-   * `small <= _ + k` and `small` is the "small side" of of a relational comparison that checks
+   * `small <= _ + k` and `small` is the "small side" of a relational comparison that checks
    * whether `small <= size` where `size` is the size of an allocation.
    */
   private Instruction getABarrierInstruction0(int delta, int k) {