From bd09aad7d54e195db134b53f087ff648c36c470c Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Mon, 26 Jan 2026 21:18:57 +0000
Subject: [PATCH 1/8] C++: Add tests.

---
 .../dataflow-tests/test-source-sink.expected  | 36 +++++++++++
 .../dataflow/dataflow-tests/test.cpp          | 60 +++++++++++++++++++
 2 files changed, 96 insertions(+)

diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
index d9ac3c3dee56..03a106208a5b 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
@@ -147,6 +147,29 @@ astFlow
 | test.cpp:1165:10:1165:15 | call to source | test.cpp:1239:10:1239:26 | * ... |
 | test.cpp:1195:10:1195:24 | call to indirect_source | test.cpp:1200:19:1200:36 | global_int_ptr_ptr |
 | test.cpp:1195:10:1195:24 | call to indirect_source | test.cpp:1201:10:1201:27 | global_int_ptr_ptr |
+| test.cpp:1258:11:1258:16 | call to source | test.cpp:1259:8:1259:10 | ... ++ |
+| test.cpp:1262:7:1262:12 | call to source | test.cpp:1263:8:1263:10 | ... -- |
+| test.cpp:1266:7:1266:12 | call to source | test.cpp:1267:8:1267:10 | ++ ... |
+| test.cpp:1266:7:1266:12 | call to source | test.cpp:1268:8:1268:8 | x |
+| test.cpp:1270:7:1270:12 | call to source | test.cpp:1271:8:1271:10 | -- ... |
+| test.cpp:1270:7:1270:12 | call to source | test.cpp:1272:8:1272:8 | x |
+| test.cpp:1274:7:1274:12 | call to source | test.cpp:1275:8:1275:14 | ... += ... |
+| test.cpp:1274:7:1274:12 | call to source | test.cpp:1276:8:1276:8 | x |
+| test.cpp:1278:7:1278:12 | call to source | test.cpp:1279:8:1279:14 | ... -= ... |
+| test.cpp:1278:7:1278:12 | call to source | test.cpp:1280:8:1280:8 | x |
+| test.cpp:1284:11:1284:16 | call to source | test.cpp:1285:8:1285:20 | ... ? ... : ... |
+| test.cpp:1288:7:1288:12 | call to source | test.cpp:1289:8:1289:20 | ... ++ |
+| test.cpp:1288:7:1288:12 | call to source | test.cpp:1290:8:1290:8 | x |
+| test.cpp:1292:7:1292:12 | call to source | test.cpp:1294:8:1294:8 | x |
+| test.cpp:1296:7:1296:12 | call to source | test.cpp:1297:8:1297:18 | ... ? ... : ... |
+| test.cpp:1296:7:1296:12 | call to source | test.cpp:1298:8:1298:8 | x |
+| test.cpp:1300:7:1300:12 | call to source | test.cpp:1301:8:1301:18 | ... ? ... : ... |
+| test.cpp:1300:7:1300:12 | call to source | test.cpp:1302:8:1302:8 | x |
+| test.cpp:1304:7:1304:12 | call to source | test.cpp:1305:8:1305:18 | ... ? ... : ... |
+| test.cpp:1304:7:1304:12 | call to source | test.cpp:1306:8:1306:8 | x |
+| test.cpp:1308:7:1308:12 | call to source | test.cpp:1309:14:1309:16 | ... ++ |
+| test.cpp:1312:7:1312:12 | call to source | test.cpp:1313:8:1313:24 | ... ? ... : ... |
+| test.cpp:1312:7:1312:12 | call to source | test.cpp:1314:8:1314:8 | x |
 | true_upon_entry.cpp:17:11:17:16 | call to source | true_upon_entry.cpp:21:8:21:8 | x |
 | true_upon_entry.cpp:27:9:27:14 | call to source | true_upon_entry.cpp:29:8:29:8 | x |
 | true_upon_entry.cpp:33:11:33:16 | call to source | true_upon_entry.cpp:39:8:39:8 | x |
@@ -354,6 +377,19 @@ irFlow
 | test.cpp:1195:10:1195:24 | *call to indirect_source | test.cpp:1218:19:1218:36 | **global_int_ptr_ptr |
 | test.cpp:1195:10:1195:24 | *call to indirect_source | test.cpp:1224:19:1224:37 | ** ... |
 | test.cpp:1195:10:1195:24 | *call to indirect_source | test.cpp:1227:10:1227:29 | * ... |
+| test.cpp:1258:11:1258:16 | call to source | test.cpp:1259:8:1259:10 | ... ++ |
+| test.cpp:1262:7:1262:12 | call to source | test.cpp:1263:8:1263:10 | ... -- |
+| test.cpp:1284:11:1284:16 | call to source | test.cpp:1285:8:1285:20 | ... ? ... : ... |
+| test.cpp:1288:7:1288:12 | call to source | test.cpp:1290:8:1290:8 | x |
+| test.cpp:1292:7:1292:12 | call to source | test.cpp:1294:8:1294:8 | x |
+| test.cpp:1296:7:1296:12 | call to source | test.cpp:1297:8:1297:18 | ... ? ... : ... |
+| test.cpp:1296:7:1296:12 | call to source | test.cpp:1298:8:1298:8 | x |
+| test.cpp:1300:7:1300:12 | call to source | test.cpp:1301:8:1301:18 | ... ? ... : ... |
+| test.cpp:1300:7:1300:12 | call to source | test.cpp:1302:8:1302:8 | x |
+| test.cpp:1304:7:1304:12 | call to source | test.cpp:1306:8:1306:8 | x |
+| test.cpp:1308:7:1308:12 | call to source | test.cpp:1309:8:1309:16 | ... ++ |
+| test.cpp:1312:7:1312:12 | call to source | test.cpp:1313:8:1313:24 | ... ? ... : ... |
+| test.cpp:1312:7:1312:12 | call to source | test.cpp:1314:8:1314:8 | x |
 | true_upon_entry.cpp:9:11:9:16 | call to source | true_upon_entry.cpp:13:8:13:8 | x |
 | true_upon_entry.cpp:17:11:17:16 | call to source | true_upon_entry.cpp:21:8:21:8 | x |
 | true_upon_entry.cpp:27:9:27:14 | call to source | true_upon_entry.cpp:29:8:29:8 | x |
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
index 35e6a074cfd0..e1c3ef98fb74 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
@@ -1252,4 +1252,64 @@ namespace globals_without_explicit_def {
     calls_set_array();
     sink(*global_int_array); // $ ir MISSING: ast
   }
+}
+
+void crement_test1() {
+  int x = source();
+  sink(x++); // $ ir ast
+  sink(x);
+
+  x = source();
+  sink(x--); // $ ir ast
+  sink(x);
+
+  x = source();
+  sink(++x); // $ SPURIOUS: ast
+  sink(x); // $ SPURIOUS: ast
+
+  x = source();
+  sink(--x); // $ SPURIOUS: ast
+  sink(x); // $ SPURIOUS: ast
+
+  x = source();
+  sink(x += 10); // $ SPURIOUS: ast
+  sink(x); // $ SPURIOUS: ast
+
+  x = source();
+  sink(x -= 10); // $ SPURIOUS: ast
+  sink(x); // $ SPURIOUS: ast
+}
+
+void crement_test2(bool b, int y) {
+  int x = source();
+  sink(b ? x++ : x--); // $ ir ast
+  sink(x);
+
+  x = source();
+  sink((b ? x : y)++); // $ ast MISSING: ir
+  sink(x); // $ ir ast
+
+  x = source();
+  sink(++(b ? x : y));
+  sink(x); // $ ir ast
+
+  x = source();
+  sink(b ? x++ : y); // $ ir ast
+  sink(x); // $ ir ast
+
+  x = source();
+  sink(b ? x : y++); // $ ir ast
+  sink(x); // $ ir ast
+
+  x = source();
+  sink(b ? ++x : y); // $ SPURIOUS: ast
+  sink(x); // $ ir ast
+
+  x = source();
+  sink((long)x++); // $ ir ast
+  sink(x);
+
+  x = source();
+  sink(b ? (long)x++ : 0); // $ ir ast
+  sink(x); // $ ir ast
 }
\ No newline at end of file

From e0a7889b71775b0fea11baf90e928170301b738f Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Mon, 26 Jan 2026 19:19:13 +0000
Subject: [PATCH 2/8] C++: Undo the hack.

---
 .../code/cpp/ir/dataflow/internal/SsaImpl.qll  | 18 +-----------------
 .../dataflow-tests/test-source-sink.expected   |  4 ++++
 .../dataflow/dataflow-tests/test.cpp           |  8 ++++----
 3 files changed, 9 insertions(+), 21 deletions(-)

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 fb24a1db69fd..28c756576093 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
@@ -432,23 +432,7 @@ private class DirectUseImpl extends UseImpl, TDirectUseImpl {
   override string toString() { result = "Use of " + this.getSourceVariable() }
 
   final override predicate hasIndexInBlock(IRBlock block, int index) {
-    // See the comment in `ssa0`'s `OperandBasedUse` for an explanation of this
-    // predicate's implementation.
-    if this.getBase().getAst() = any(Cpp::PostfixCrementOperation c).getOperand()
-    then
-      exists(Operand op, int indirection, Instruction base |
-        indirection = this.getIndirection() and
-        base = this.getBase() and
-        op =
-          min(Operand cand, int i |
-            isUse(_, cand, base, indirection, indirectionIndex) and
-            block.getInstruction(i) = cand.getUse()
-          |
-            cand order by i
-          ) and
-        block.getInstruction(index) = op.getUse()
-      )
-    else operand.getUse() = block.getInstruction(index)
+    operand.getUse() = block.getInstruction(index)
   }
 
   private BaseSourceVariableInstruction getBase() { isUse(_, operand, result, _, indirectionIndex) }
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
index 03a106208a5b..7b5c1cd0cf09 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
@@ -378,8 +378,11 @@ irFlow
 | test.cpp:1195:10:1195:24 | *call to indirect_source | test.cpp:1224:19:1224:37 | ** ... |
 | test.cpp:1195:10:1195:24 | *call to indirect_source | test.cpp:1227:10:1227:29 | * ... |
 | test.cpp:1258:11:1258:16 | call to source | test.cpp:1259:8:1259:10 | ... ++ |
+| test.cpp:1258:11:1258:16 | call to source | test.cpp:1260:8:1260:8 | x |
 | test.cpp:1262:7:1262:12 | call to source | test.cpp:1263:8:1263:10 | ... -- |
+| test.cpp:1262:7:1262:12 | call to source | test.cpp:1264:8:1264:8 | x |
 | test.cpp:1284:11:1284:16 | call to source | test.cpp:1285:8:1285:20 | ... ? ... : ... |
+| test.cpp:1284:11:1284:16 | call to source | test.cpp:1286:8:1286:8 | x |
 | test.cpp:1288:7:1288:12 | call to source | test.cpp:1290:8:1290:8 | x |
 | test.cpp:1292:7:1292:12 | call to source | test.cpp:1294:8:1294:8 | x |
 | test.cpp:1296:7:1296:12 | call to source | test.cpp:1297:8:1297:18 | ... ? ... : ... |
@@ -388,6 +391,7 @@ irFlow
 | test.cpp:1300:7:1300:12 | call to source | test.cpp:1302:8:1302:8 | x |
 | test.cpp:1304:7:1304:12 | call to source | test.cpp:1306:8:1306:8 | x |
 | test.cpp:1308:7:1308:12 | call to source | test.cpp:1309:8:1309:16 | ... ++ |
+| test.cpp:1308:7:1308:12 | call to source | test.cpp:1310:8:1310:8 | x |
 | test.cpp:1312:7:1312:12 | call to source | test.cpp:1313:8:1313:24 | ... ? ... : ... |
 | test.cpp:1312:7:1312:12 | call to source | test.cpp:1314:8:1314:8 | x |
 | true_upon_entry.cpp:9:11:9:16 | call to source | true_upon_entry.cpp:13:8:13:8 | x |
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
index e1c3ef98fb74..e42a5652729d 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
@@ -1257,11 +1257,11 @@ namespace globals_without_explicit_def {
 void crement_test1() {
   int x = source();
   sink(x++); // $ ir ast
-  sink(x);
+  sink(x); // $ SPURIOUS: ir
 
   x = source();
   sink(x--); // $ ir ast
-  sink(x);
+  sink(x); // $ SPURIOUS: ir
 
   x = source();
   sink(++x); // $ SPURIOUS: ast
@@ -1283,7 +1283,7 @@ void crement_test1() {
 void crement_test2(bool b, int y) {
   int x = source();
   sink(b ? x++ : x--); // $ ir ast
-  sink(x);
+  sink(x); // $ SPURIOUS: ir
 
   x = source();
   sink((b ? x : y)++); // $ ast MISSING: ir
@@ -1307,7 +1307,7 @@ void crement_test2(bool b, int y) {
 
   x = source();
   sink((long)x++); // $ ir ast
-  sink(x);
+  sink(x); // $ SPURIOUS: ir
 
   x = source();
   sink(b ? (long)x++ : 0); // $ ir ast

From 3d445be926d574710c8f784f808ef68102debfac Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Mon, 26 Jan 2026 16:30:38 +0000
Subject: [PATCH 3/8] C++: Small refactor.

---
 .../code/cpp/ir/dataflow/internal/SsaImpl.qll | 100 +++++++++---------
 1 file changed, 52 insertions(+), 48 deletions(-)

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 28c756576093..81f91a0814c3 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
@@ -223,19 +223,8 @@ abstract class DefImpl extends TDefImpl {
    */
   abstract int getIndirection();
 
-  /**
-   * Gets the base source variable (i.e., the variable without
-   * any indirection) of this definition or use.
-   */
-  abstract BaseSourceVariable getBaseSourceVariable();
-
   /** Gets the variable that is defined or used. */
-  SourceVariable getSourceVariable() {
-    exists(BaseSourceVariable v, int indirection |
-      sourceVariableHasBaseAndIndex(result, v, indirection) and
-      defHasSourceVariable(this, v, indirection)
-    )
-  }
+  abstract SourceVariable getSourceVariable();
 
   /**
    * Holds if this definition is guaranteed to totally overwrite the
@@ -293,19 +282,8 @@ abstract class UseImpl extends TUseImpl {
   /** Gets the indirection index of this use. */
   final int getIndirectionIndex() { result = indirectionIndex }
 
-  /**
-   * Gets the base source variable (i.e., the variable without
-   * any indirection) of this definition or use.
-   */
-  abstract BaseSourceVariable getBaseSourceVariable();
-
   /** Gets the variable that is defined or used. */
-  SourceVariable getSourceVariable() {
-    exists(BaseSourceVariable v, int indirection |
-      sourceVariableHasBaseAndIndex(result, v, indirection) and
-      useHasSourceVariable(this, v, indirection)
-    )
-  }
+  abstract SourceVariable getSourceVariable();
 
   /**
    * Holds if this use is guaranteed to read the
@@ -314,18 +292,6 @@ abstract class UseImpl extends TUseImpl {
   abstract predicate isCertain();
 }
 
-pragma[noinline]
-private predicate defHasSourceVariable(DefImpl def, BaseSourceVariable bv, int ind) {
-  bv = def.getBaseSourceVariable() and
-  ind = def.getIndirection()
-}
-
-pragma[noinline]
-private predicate useHasSourceVariable(UseImpl use, BaseSourceVariable bv, int ind) {
-  bv = use.getBaseSourceVariable() and
-  ind = use.getIndirection()
-}
-
 pragma[noinline]
 private predicate sourceVariableHasBaseAndIndex(SourceVariable v, BaseSourceVariable bv, int ind) {
   v.getBaseVariable() = bv and
@@ -366,8 +332,6 @@ abstract private class DefAddressImpl extends DefImpl, TDefAddressImpl {
     result.getBaseVariable() = v and
     result.getIndirection() = 0
   }
-
-  final override BaseSourceVariable getBaseSourceVariable() { result = v }
 }
 
 private class DefVariableAddressImpl extends DefAddressImpl {
@@ -413,8 +377,17 @@ private class DirectDef extends DefImpl, TDirectDefImpl {
     isDef(_, _, address, result, _, indirectionIndex)
   }
 
-  override BaseSourceVariable getBaseSourceVariable() {
-    result = this.getBase().getBaseSourceVariable()
+  pragma[nomagic]
+  private predicate hasBaseSourceVariableAndIndirection(BaseSourceVariable v, int indirection) {
+    v = this.getBase().getBaseSourceVariable() and
+    indirection = this.getIndirection()
+  }
+
+  final override SourceVariable getSourceVariable() {
+    exists(BaseSourceVariable v, int indirection |
+      sourceVariableHasBaseAndIndex(result, v, indirection) and
+      this.hasBaseSourceVariableAndIndirection(v, indirection)
+    )
   }
 
   override int getIndirection() { isDef(_, _, address, _, result, indirectionIndex) }
@@ -437,8 +410,17 @@ private class DirectUseImpl extends UseImpl, TDirectUseImpl {
 
   private BaseSourceVariableInstruction getBase() { isUse(_, operand, result, _, indirectionIndex) }
 
-  override BaseSourceVariable getBaseSourceVariable() {
-    result = this.getBase().getBaseSourceVariable()
+  pragma[nomagic]
+  private predicate hasBaseSourceVariableAndIndirection(BaseSourceVariable bv, int indirection) {
+    this.getBase().getBaseSourceVariable() = bv and
+    this.getIndirection() = indirection
+  }
+
+  override SourceVariable getSourceVariable() {
+    exists(BaseSourceVariable v, int indirection |
+      sourceVariableHasBaseAndIndex(result, v, indirection) and
+      this.hasBaseSourceVariableAndIndirection(v, indirection)
+    )
   }
 
   final Operand getOperand() { result = operand }
@@ -516,7 +498,18 @@ class FinalParameterUse extends UseImpl, TFinalParameterUse {
     result instanceof UnknownLocation
   }
 
-  override BaseIRVariable getBaseSourceVariable() { result.getIRVariable().getAst() = p }
+  pragma[nomagic]
+  private predicate hasBaseSourceVariableAndIndirectrion(BaseIRVariable v, int indirection) {
+    v.getIRVariable().getAst() = p and
+    indirection = this.getIndirection()
+  }
+
+  override SourceVariable getSourceVariable() {
+    exists(BaseIRVariable v, int indirection |
+      sourceVariableHasBaseAndIndex(result, v, indirection) and
+      this.hasBaseSourceVariableAndIndirectrion(v, indirection)
+    )
+  }
 }
 
 /**
@@ -596,8 +589,17 @@ class GlobalUse extends UseImpl, TGlobalUse {
     hasReturnPosition(f, block, index)
   }
 
-  override BaseSourceVariable getBaseSourceVariable() {
-    baseSourceVariableIsGlobal(result, global, f)
+  pragma[nomagic]
+  private predicate hasBaseSourceVariableAndIndirection(BaseIRVariable v, int indirection) {
+    baseSourceVariableIsGlobal(v, global, f) and
+    indirection = this.getIndirection()
+  }
+
+  override SourceVariable getSourceVariable() {
+    exists(BaseIRVariable v, int indirection |
+      sourceVariableHasBaseAndIndex(result, v, indirection) and
+      this.hasBaseSourceVariableAndIndirection(v, indirection)
+    )
   }
 
   final override Cpp::Location getLocation() { result = f.getLocation() }
@@ -642,9 +644,11 @@ class GlobalDefImpl extends DefImpl, TGlobalDefImpl {
     )
   }
 
-  /** Gets the global variable associated with this definition. */
-  override BaseSourceVariable getBaseSourceVariable() {
-    baseSourceVariableIsGlobal(result, global, f)
+  final override SourceVariable getSourceVariable() {
+    exists(BaseSourceVariable v |
+      sourceVariableHasBaseAndIndex(result, v, indirectionIndex) and
+      baseSourceVariableIsGlobal(v, global, f)
+    )
   }
 
   override int getIndirection() { result = indirectionIndex }

From db3f22a2e873523a4018708838c90f7c64c3547e Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Mon, 26 Jan 2026 20:43:45 +0000
Subject: [PATCH 4/8] C++: Another small refactor.

---
 .../lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll  | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

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 81f91a0814c3..c7f622f81d39 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
@@ -232,8 +232,8 @@ abstract class DefImpl extends TDefImpl {
    */
   abstract predicate isCertain();
 
-  /** Gets the value written to the destination variable by this definition. */
-  abstract Node0Impl getValue();
+  /** Gets the value written to the destination variable by this definition, if any. */
+  Node0Impl getValue() { none() }
 
   /** Gets the operand that represents the address of this definition, if any. */
   Operand getAddressOperand() { none() }
@@ -324,8 +324,6 @@ abstract private class DefAddressImpl extends DefImpl, TDefAddressImpl {
 
   final override predicate isCertain() { any() }
 
-  final override Node0Impl getValue() { none() }
-
   override Cpp::Location getLocation() { result = v.getLocation() }
 
   final override SourceVariable getSourceVariable() {
@@ -653,8 +651,6 @@ class GlobalDefImpl extends DefImpl, TGlobalDefImpl {
 
   override int getIndirection() { result = indirectionIndex }
 
-  override Node0Impl getValue() { none() }
-
   override predicate isCertain() { any() }
 
   /**

From 445cca1432747f7803beb8636bd4dada8dc33366 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 27 Jan 2026 18:29:12 +0000
Subject: [PATCH 5/8] C++: Proper SSA support for post-crement reads.

---
 .../code/cpp/ir/dataflow/internal/SsaImpl.qll | 223 ++++++++++++++++--
 1 file changed, 209 insertions(+), 14 deletions(-)

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 c7f622f81d39..7877c55d2000 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
@@ -15,17 +15,79 @@ private import DataFlowPrivate
 import SsaImplCommon
 
 private module SourceVariables {
+  /**
+   * Holds if `store` is the `StoreInstruction` generated by an postfix
+   * increment or decrement operation `e`, and `postCrement` is the operand
+   * that represents the use of the evaluated value of `e`.
+   */
+  private predicate isUseAfterPostfixCrement0(StoreInstruction store, Operand postCrement) {
+    exists(
+      BinaryInstruction binary, IRBlock b, int iPre, int iPost, int iStore, Operand preCrement,
+      Instruction left
+    |
+      binary instanceof AddInstruction
+      or
+      binary instanceof PointerAddInstruction
+      or
+      binary instanceof SubInstruction
+      or
+      binary instanceof PointerSubInstruction
+    |
+      store.getSourceValue() = binary and
+      left = binary.getLeft() and
+      strictcount(left.getAUse()) = 2 and
+      left.getAUse() = preCrement and
+      left.getAUse() = postCrement and
+      b.getInstruction(iPre) = preCrement.getUse() and
+      b.getInstruction(iPost) = postCrement.getUse() and
+      b.getInstruction(iStore) = store and
+      iPre < iStore and
+      iStore < iPost
+    )
+  }
+
+  /**
+   * Holds if `store` is the `StoreInstruction` generated by an postfix
+   * increment or decrement operation `e`, and `postCrement` is the fully
+   * converted operand that represents the use of the evaluated value of `e`.
+   */
+  private predicate isUseAfterPostfixCrement(StoreInstruction store, Operand postCrement) {
+    isUseAfterPostfixCrement0(store, postCrement) and
+    conversionFlow(postCrement, _, false, _)
+    or
+    exists(Instruction instr, Operand postCrement0 |
+      isUseAfterPostfixCrement(store, postCrement0) and
+      conversionFlow(postCrement0, instr, false, _) and
+      instr = postCrement.getDef()
+    )
+  }
+
+  private predicate hasSavedPostfixCrementSourceVariable(
+    BaseSourceVariable base, StoreInstruction store, int ind
+  ) {
+    exists(BaseSourceVariableInstruction inst, int ind0 |
+      isUseAfterPostfixCrement(store, _) and
+      inst.getBaseSourceVariable() = base and
+      isDef(_, _, store.getDestinationAddressOperand(), inst, ind0, 0) and
+      ind = [ind0 .. countIndirectionsForCppType(base.getLanguageType()) + 1]
+    )
+  }
+
   cached
   private newtype TSourceVariable =
-    TMkSourceVariable(BaseSourceVariable base, int ind) {
+    TNormalSourceVariable(BaseSourceVariable base, int ind) {
       ind = [0 .. countIndirectionsForCppType(base.getLanguageType()) + 1]
+    } or
+    TSavedPostfixCrementSourceVariable(StoreInstruction store, int ind) {
+      hasSavedPostfixCrementSourceVariable(_, store, ind)
     }
 
-  class SourceVariable extends TSourceVariable {
+  abstract private class AbstractSourceVariable extends TSourceVariable {
     BaseSourceVariable base;
     int ind;
 
-    SourceVariable() { this = TMkSourceVariable(base, ind) }
+    bindingset[ind]
+    AbstractSourceVariable() { any() }
 
     /** Gets the IR variable associated with this `SourceVariable`, if any. */
     IRVariable getIRVariable() { result = base.(BaseIRVariable).getIRVariable() }
@@ -37,7 +99,7 @@ private module SourceVariables {
     BaseSourceVariable getBaseVariable() { result = base }
 
     /** Gets a textual representation of this element. */
-    string toString() { result = repeatStars(this.getIndirection()) + base.toString() }
+    abstract string toString();
 
     /**
      * Gets the number of loads performed on the base source variable
@@ -62,6 +124,53 @@ private module SourceVariables {
     /** Gets the location of this variable. */
     Location getLocation() { result = this.getBaseVariable().getLocation() }
   }
+
+  final class SourceVariable = AbstractSourceVariable;
+
+  /**
+   * A regular source variable. Most source variables are instances of this
+   * class.
+   */
+  class NormalSourceVariable extends AbstractSourceVariable, TNormalSourceVariable {
+    NormalSourceVariable() { this = TNormalSourceVariable(base, ind) }
+
+    final override string toString() {
+      result = repeatStars(this.getIndirection()) + base.toString()
+    }
+  }
+
+  /**
+   * Before a value is postfix incremented (or decremented) we "save" its
+   * current value so that the pre-incremented value can be returned to the
+   * enclosing expression. We use the source variables represented by this
+   * class to represent the "saved value".
+   */
+  class SavedPostfixCrementSourceVariable extends AbstractSourceVariable,
+    TSavedPostfixCrementSourceVariable
+  {
+    StoreInstruction store;
+
+    SavedPostfixCrementSourceVariable() {
+      this = TSavedPostfixCrementSourceVariable(store, ind) and
+      hasSavedPostfixCrementSourceVariable(base, store, ind)
+    }
+
+    final override string toString() {
+      result = repeatStars(this.getIndirection()) + base.toString() + " [before crement]"
+    }
+
+    /**
+     * Gets the `StoreInstruction` that writes the incremented (or decremented)
+     * value.
+     */
+    StoreInstruction getStoreInstruction() { result = store }
+
+    /**
+     * Gets the fully converted `Operand` that represents the use of the
+     * value before the increment.
+     */
+    Operand getOperand() { isUseAfterPostfixCrement(store, result) }
+  }
 }
 
 import SourceVariables
@@ -109,17 +218,43 @@ private newtype TDefImpl =
   TDirectDefImpl(Operand address, int indirectionIndex) {
     isDef(_, _, address, _, _, indirectionIndex)
   } or
+  TSavedPostfixCrementDefImpl(SavedPostfixCrementSourceVariable sv, int indirectionIndex) {
+    isDef(_, _, sv.getStoreInstruction().getDestinationAddressOperand(), _, sv.getIndirection(),
+      indirectionIndex)
+  } or
   TGlobalDefImpl(GlobalLikeVariable v, IRFunction f, int indirectionIndex) {
     // Represents the initial "definition" of a global variable when entering
     // a function body.
     isGlobalDefImpl(v, f, _, indirectionIndex)
   }
 
+pragma[nomagic]
+private predicate hasOperandAndIndirection(
+  SavedPostfixCrementSourceVariable sv, Operand operand, int indirection
+) {
+  sv.getOperand() = operand and
+  sv.getIndirection() = indirection
+}
+
+private predicate hasBeforePostCrementUseImpl(
+  SavedPostfixCrementSourceVariable sv, Operand operand, int indirectionIndex
+) {
+  not isDef(true, _, operand, _, _, _) and
+  exists(int indirection |
+    hasOperandAndIndirection(sv, operand, indirection) and
+    isUse(_, operand, _, indirection, indirectionIndex)
+  )
+}
+
 cached
 private newtype TUseImpl =
   TDirectUseImpl(Operand operand, int indirectionIndex) {
     isUse(_, operand, _, _, indirectionIndex) and
-    not isDef(true, _, operand, _, _, _)
+    not isDef(true, _, operand, _, _, _) and
+    not hasBeforePostCrementUseImpl(_, operand, indirectionIndex)
+  } or
+  TSavedPostfixCrementUseImpl(SavedPostfixCrementSourceVariable sv, int indirectionIndex) {
+    hasBeforePostCrementUseImpl(sv, _, indirectionIndex)
   } or
   TGlobalUse(GlobalLikeVariable v, IRFunction f, int indirectionIndex) {
     // Represents a final "use" of a global variable to ensure that
@@ -326,7 +461,7 @@ abstract private class DefAddressImpl extends DefImpl, TDefAddressImpl {
 
   override Cpp::Location getLocation() { result = v.getLocation() }
 
-  final override SourceVariable getSourceVariable() {
+  final override NormalSourceVariable getSourceVariable() {
     result.getBaseVariable() = v and
     result.getIndirection() = 0
   }
@@ -381,7 +516,7 @@ private class DirectDef extends DefImpl, TDirectDefImpl {
     indirection = this.getIndirection()
   }
 
-  final override SourceVariable getSourceVariable() {
+  final override NormalSourceVariable getSourceVariable() {
     exists(BaseSourceVariable v, int indirection |
       sourceVariableHasBaseAndIndex(result, v, indirection) and
       this.hasBaseSourceVariableAndIndirection(v, indirection)
@@ -395,6 +530,32 @@ private class DirectDef extends DefImpl, TDirectDefImpl {
   override predicate isCertain() { isDef(true, _, address, _, _, indirectionIndex) }
 }
 
+/**
+ * A definition that "saves" the value of a variable before it is incremented
+ * or decremented.
+ */
+private class SavedPostfixCrementDefImpl extends DefImpl, TSavedPostfixCrementDefImpl {
+  SavedPostfixCrementSourceVariable sv;
+
+  SavedPostfixCrementDefImpl() { this = TSavedPostfixCrementDefImpl(sv, indirectionIndex) }
+
+  override Cpp::Location getLocation() { result = sv.getStoreInstruction().getLocation() }
+
+  final override predicate hasIndexInBlock(IRBlock block, int index) {
+    sv.getStoreInstruction() = block.getInstruction(index)
+  }
+
+  override string toString() { result = "Def of " + this.getSourceVariable() }
+
+  override SourceVariable getSourceVariable() { result = sv }
+
+  override int getIndirection() { result = sv.getIndirection() }
+
+  override predicate isCertain() {
+    isDef(true, _, sv.getStoreInstruction().getDestinationAddressOperand(), _, _, indirectionIndex)
+  }
+}
+
 private class DirectUseImpl extends UseImpl, TDirectUseImpl {
   Operand operand;
 
@@ -414,7 +575,7 @@ private class DirectUseImpl extends UseImpl, TDirectUseImpl {
     this.getIndirection() = indirection
   }
 
-  override SourceVariable getSourceVariable() {
+  override NormalSourceVariable getSourceVariable() {
     exists(BaseSourceVariable v, int indirection |
       sourceVariableHasBaseAndIndex(result, v, indirection) and
       this.hasBaseSourceVariableAndIndirection(v, indirection)
@@ -432,6 +593,34 @@ private class DirectUseImpl extends UseImpl, TDirectUseImpl {
   override Node getNode() { nodeHasOperand(result, operand, indirectionIndex) }
 }
 
+/**
+ * The use of the original "saved" variable after the variable has been incremented
+ * or decremented.
+ */
+private class SavedPostfixCrementUseImpl extends UseImpl, TSavedPostfixCrementUseImpl {
+  SavedPostfixCrementSourceVariable sv;
+
+  SavedPostfixCrementUseImpl() { this = TSavedPostfixCrementUseImpl(sv, indirectionIndex) }
+
+  override string toString() { result = "Use of " + this.getSourceVariable() }
+
+  final override predicate hasIndexInBlock(IRBlock block, int index) {
+    this.getOperand().getUse() = block.getInstruction(index)
+  }
+
+  override SourceVariable getSourceVariable() { result = sv }
+
+  final Operand getOperand() { result = sv.getOperand() }
+
+  final override Cpp::Location getLocation() { result = this.getOperand().getLocation() }
+
+  override int getIndirection() { result = sv.getIndirection() }
+
+  override predicate isCertain() { isUse(true, this.getOperand(), _, _, indirectionIndex) }
+
+  override Node getNode() { nodeHasOperand(result, this.getOperand(), indirectionIndex) }
+}
+
 pragma[nomagic]
 private predicate finalParameterNodeHasParameterAndIndex(
   FinalParameterNode n, Parameter p, int indirectionIndex
@@ -502,7 +691,7 @@ class FinalParameterUse extends UseImpl, TFinalParameterUse {
     indirection = this.getIndirection()
   }
 
-  override SourceVariable getSourceVariable() {
+  override NormalSourceVariable getSourceVariable() {
     exists(BaseIRVariable v, int indirection |
       sourceVariableHasBaseAndIndex(result, v, indirection) and
       this.hasBaseSourceVariableAndIndirectrion(v, indirection)
@@ -593,7 +782,7 @@ class GlobalUse extends UseImpl, TGlobalUse {
     indirection = this.getIndirection()
   }
 
-  override SourceVariable getSourceVariable() {
+  override NormalSourceVariable getSourceVariable() {
     exists(BaseIRVariable v, int indirection |
       sourceVariableHasBaseAndIndex(result, v, indirection) and
       this.hasBaseSourceVariableAndIndirection(v, indirection)
@@ -642,7 +831,7 @@ class GlobalDefImpl extends DefImpl, TGlobalDefImpl {
     )
   }
 
-  final override SourceVariable getSourceVariable() {
+  final override NormalSourceVariable getSourceVariable() {
     exists(BaseSourceVariable v |
       sourceVariableHasBaseAndIndex(result, v, indirectionIndex) and
       baseSourceVariableIsGlobal(v, global, f)
@@ -688,9 +877,15 @@ predicate defToNode(Node node, Definition def, SourceVariable sv) {
 }
 
 private predicate defToNode(Node node, Definition def) {
-  nodeHasOperand(node, def.getValue().asOperand(), def.getIndirectionIndex())
-  or
-  nodeHasInstruction(node, def.getValue().asInstruction(), def.getIndirectionIndex())
+  // Only definitions of `NormalSourceVariable` need to be converted into
+  // dataflow nodes. The other case, `SavedPostfixCrementSourceVariable`,
+  // are internal definitions that don't have a dataflow node representation.
+  def.getSourceVariable() instanceof NormalSourceVariable and
+  (
+    nodeHasOperand(node, def.getValue().asOperand(), def.getIndirectionIndex())
+    or
+    nodeHasInstruction(node, def.getValue().asInstruction(), def.getIndirectionIndex())
+  )
   or
   node.(InitialGlobalValue).getGlobalDef() = def
 }

From 28fec0c12951dc8a69acfb8c51c02341f33769a3 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 27 Jan 2026 18:29:21 +0000
Subject: [PATCH 6/8] C++: Accept test changes.

---
 .../dataflow/dataflow-tests/test-source-sink.expected     | 4 ----
 .../test/library-tests/dataflow/dataflow-tests/test.cpp   | 8 ++++----
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
index 7b5c1cd0cf09..03a106208a5b 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected
@@ -378,11 +378,8 @@ irFlow
 | test.cpp:1195:10:1195:24 | *call to indirect_source | test.cpp:1224:19:1224:37 | ** ... |
 | test.cpp:1195:10:1195:24 | *call to indirect_source | test.cpp:1227:10:1227:29 | * ... |
 | test.cpp:1258:11:1258:16 | call to source | test.cpp:1259:8:1259:10 | ... ++ |
-| test.cpp:1258:11:1258:16 | call to source | test.cpp:1260:8:1260:8 | x |
 | test.cpp:1262:7:1262:12 | call to source | test.cpp:1263:8:1263:10 | ... -- |
-| test.cpp:1262:7:1262:12 | call to source | test.cpp:1264:8:1264:8 | x |
 | test.cpp:1284:11:1284:16 | call to source | test.cpp:1285:8:1285:20 | ... ? ... : ... |
-| test.cpp:1284:11:1284:16 | call to source | test.cpp:1286:8:1286:8 | x |
 | test.cpp:1288:7:1288:12 | call to source | test.cpp:1290:8:1290:8 | x |
 | test.cpp:1292:7:1292:12 | call to source | test.cpp:1294:8:1294:8 | x |
 | test.cpp:1296:7:1296:12 | call to source | test.cpp:1297:8:1297:18 | ... ? ... : ... |
@@ -391,7 +388,6 @@ irFlow
 | test.cpp:1300:7:1300:12 | call to source | test.cpp:1302:8:1302:8 | x |
 | test.cpp:1304:7:1304:12 | call to source | test.cpp:1306:8:1306:8 | x |
 | test.cpp:1308:7:1308:12 | call to source | test.cpp:1309:8:1309:16 | ... ++ |
-| test.cpp:1308:7:1308:12 | call to source | test.cpp:1310:8:1310:8 | x |
 | test.cpp:1312:7:1312:12 | call to source | test.cpp:1313:8:1313:24 | ... ? ... : ... |
 | test.cpp:1312:7:1312:12 | call to source | test.cpp:1314:8:1314:8 | x |
 | true_upon_entry.cpp:9:11:9:16 | call to source | true_upon_entry.cpp:13:8:13:8 | x |
diff --git a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
index e42a5652729d..e1c3ef98fb74 100644
--- a/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
+++ b/cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp
@@ -1257,11 +1257,11 @@ namespace globals_without_explicit_def {
 void crement_test1() {
   int x = source();
   sink(x++); // $ ir ast
-  sink(x); // $ SPURIOUS: ir
+  sink(x);
 
   x = source();
   sink(x--); // $ ir ast
-  sink(x); // $ SPURIOUS: ir
+  sink(x);
 
   x = source();
   sink(++x); // $ SPURIOUS: ast
@@ -1283,7 +1283,7 @@ void crement_test1() {
 void crement_test2(bool b, int y) {
   int x = source();
   sink(b ? x++ : x--); // $ ir ast
-  sink(x); // $ SPURIOUS: ir
+  sink(x);
 
   x = source();
   sink((b ? x : y)++); // $ ast MISSING: ir
@@ -1307,7 +1307,7 @@ void crement_test2(bool b, int y) {
 
   x = source();
   sink((long)x++); // $ ir ast
-  sink(x); // $ SPURIOUS: ir
+  sink(x);
 
   x = source();
   sink(b ? (long)x++ : 0); // $ ir ast

From 4503c625b4c1682eae76948b71bf15d5bad689ff Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Tue, 27 Jan 2026 19:02:28 +0000
Subject: [PATCH 7/8] C++: Implement copilot suggestions.

---
 cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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 7877c55d2000..64840c84c780 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
@@ -16,7 +16,7 @@ import SsaImplCommon
 
 private module SourceVariables {
   /**
-   * Holds if `store` is the `StoreInstruction` generated by an postfix
+   * Holds if `store` is the `StoreInstruction` generated by n postfix
    * increment or decrement operation `e`, and `postCrement` is the operand
    * that represents the use of the evaluated value of `e`.
    */
@@ -686,7 +686,7 @@ class FinalParameterUse extends UseImpl, TFinalParameterUse {
   }
 
   pragma[nomagic]
-  private predicate hasBaseSourceVariableAndIndirectrion(BaseIRVariable v, int indirection) {
+  private predicate hasBaseSourceVariableAndIndirection(BaseIRVariable v, int indirection) {
     v.getIRVariable().getAst() = p and
     indirection = this.getIndirection()
   }
@@ -694,7 +694,7 @@ class FinalParameterUse extends UseImpl, TFinalParameterUse {
   override NormalSourceVariable getSourceVariable() {
     exists(BaseIRVariable v, int indirection |
       sourceVariableHasBaseAndIndex(result, v, indirection) and
-      this.hasBaseSourceVariableAndIndirectrion(v, indirection)
+      this.hasBaseSourceVariableAndIndirection(v, indirection)
     )
   }
 }

From 61a53fadc0b78352a7c45e5925488a67bc202931 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Thu, 29 Jan 2026 11:50:44 +0000
Subject: [PATCH 8/8] C++: Fix spelling.

---
 cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 64840c84c780..80b440fff221 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
@@ -16,7 +16,7 @@ import SsaImplCommon
 
 private module SourceVariables {
   /**
-   * Holds if `store` is the `StoreInstruction` generated by n postfix
+   * Holds if `store` is the `StoreInstruction` generated by a postfix
    * increment or decrement operation `e`, and `postCrement` is the operand
    * that represents the use of the evaluated value of `e`.
    */