C++: New, behaviour preserving solution.

Author: geoffw0

cpp/ql/lib/semmle/code/cpp/commons/NullTermination.qll

@@ -3,8 +3,17 @@ private import semmle.code.cpp.models.interfaces.ArrayFunction
 private import semmle.code.cpp.models.implementations.Strcat
 import semmle.code.cpp.dataflow.DataFlow
 
+private predicate mayAddNullTerminatorHelper(Expr e, VariableAccess va, Expr e0) {
+  exists(StackVariable v0, Expr val |
+    exprDefinition(v0, e, val) and
+    val.getAChild*() = va and
+    mayAddNullTerminator(e0, v0.getAnAccess())
+  )
+}
+
 /**
- * Holds if the expression `e` may add a null terminator to the string in `va`.
+ * Holds if the expression `e` may add a null terminator to the string in
+ * variable `v`.
  */
 predicate mayAddNullTerminator(Expr e, VariableAccess va) {
   // Assignment: dereferencing or array access
@@ -21,10 +30,14 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
   )
   or
   // Assignment to another stack variable
-  exists(StackVariable v0, Expr val |
-    exprDefinition(v0, e, val) and // e resembles `v0 := val`
-    val.getAChild*() = va and
-    mayAddNullTerminator(_, v0.getAnAccess())
+  exists(Expr e0, BasicBlock bb, int pos, BasicBlock bb0, int pos0 |
+    mayAddNullTerminatorHelper(pragma[only_bind_into](e), va, pragma[only_bind_into](e0)) and
+    pragma[only_bind_into](bb).getNode(pos) = e and
+    pragma[only_bind_into](bb0).getNode(pos0) = e0
+  |
+    bb = bb0 and pos < pos0
+    or
+    bb.getASuccessor+() = bb0
   )
   or
   // Assignment to non-stack variable