From 795b138584399b5cc162413d35cf5d9b07d8660e Mon Sep 17 00:00:00 2001
From: Taus <tausbn@github.com>
Date: Tue, 28 Apr 2026 15:06:30 +0000
Subject: [PATCH 1/5] Python: Add self-validating CFG tests

These tests consist of various Python constructions (hopefully a
somewhat comprehensive set) with specific timestamp annotations
scattered throughout. When the tests are run using the Python 3
interpreter, these annotations are checked and compared to the "current
timestamp" to see that they are in agreement. This is what makes the
tests "self-validating".

There are a few different kinds of annotations: the basic `t[4]` style
(meaning this is executed at timestamp 4), the `t[dead(4)]` variant
(meaning this _would_ happen at timestamp 4, but it is in a dead
branch), and `t[never]` (meaning this is never executed at all).

In addition to this, there is a query, MissingAnnotations, which checks
whether we have applied these annotations maximally. Many expression
nodes are not actually annotatable, so there is a sizeable list of
excluded nodes for that query.
---
 .../MissingAnnotations.expected               |   0
 .../evaluation-order/MissingAnnotations.ql    |  15 +
 .../evaluation-order/OldCfgImpl.qll           |  16 +
 .../evaluation-order/TimerUtils.qll           | 620 ++++++++++++++++++
 .../evaluation-order/test_assert_raise.py     |  56 ++
 .../evaluation-order/test_async.py            |  97 +++
 .../evaluation-order/test_augassign.py        |  53 ++
 .../evaluation-order/test_basic.py            | 223 +++++++
 .../evaluation-order/test_boolean.py          |  76 +++
 .../evaluation-order/test_classes.py          |  74 +++
 .../evaluation-order/test_comprehensions.py   |  46 ++
 .../evaluation-order/test_conditional.py      |  44 ++
 .../evaluation-order/test_fstring.py          |  34 +
 .../evaluation-order/test_functions.py        |  85 +++
 .../ControlFlow/evaluation-order/test_if.py   | 114 ++++
 .../evaluation-order/test_lambda.py           |  46 ++
 .../evaluation-order/test_loops.py            | 146 +++++
 .../evaluation-order/test_match.py            | 173 +++++
 .../ControlFlow/evaluation-order/test_try.py  | 182 +++++
 .../evaluation-order/test_unpacking.py        |  48 ++
 .../ControlFlow/evaluation-order/test_with.py |  58 ++
 .../evaluation-order/test_yield.py            | 105 +++
 .../ControlFlow/evaluation-order/timer.py     | 189 ++++++
 23 files changed, 2500 insertions(+)
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/MissingAnnotations.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/MissingAnnotations.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/OldCfgImpl.qll
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_async.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_augassign.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_classes.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_comprehensions.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_fstring.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_functions.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_lambda.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_unpacking.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_with.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/test_yield.py
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py

diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/MissingAnnotations.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/MissingAnnotations.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/MissingAnnotations.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/MissingAnnotations.ql
new file mode 100644
index 000000000000..51f324e9399c
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/MissingAnnotations.ql
@@ -0,0 +1,15 @@
+/**
+ * Finds expressions in test functions that lack a timer annotation
+ * and are not part of the timer mechanism or otherwise excluded.
+ * An empty result means every annotatable expression is covered.
+ */
+
+import python
+import TimerUtils
+
+from TestFunction f, Expr e
+where
+  e.getScope().getEnclosingScope*() = f and
+  not isTimerMechanism(e, f) and
+  not isUnannotatable(e)
+select e, "Missing annotation in $@", f, f.getName()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/OldCfgImpl.qll b/python/ql/test/library-tests/ControlFlow/evaluation-order/OldCfgImpl.qll
new file mode 100644
index 000000000000..fc52c8dd3ed1
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/OldCfgImpl.qll
@@ -0,0 +1,16 @@
+/**
+ * Implementation of the evaluation-order CFG signature using the existing
+ * Python control flow graph.
+ */
+
+private import python as Py
+import TimerUtils
+
+/** Existing Python CFG implementation of the evaluation-order signature. */
+module OldCfg implements EvalOrderCfgSig {
+  class CfgNode = Py::ControlFlowNode;
+
+  class BasicBlock = Py::BasicBlock;
+
+  CfgNode scopeGetEntryNode(Py::Scope s) { result = s.getEntryNode() }
+}
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll b/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll
new file mode 100644
index 000000000000..717138e89bae
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll
@@ -0,0 +1,620 @@
+/**
+ * Utility library for identifying timer annotations in evaluation-order tests.
+ *
+ * Identifies `expr @ t[n]` (matmul), `t(expr, n)` (call), and
+ * `expr @ t.dead[n]` (dead-code) patterns, extracts timestamp values,
+ * and provides predicates for traversing consecutive annotated CFG nodes.
+ */
+
+private import python
+
+/**
+ * A function decorated with `@test` from the timer module.
+ * The first parameter is the timer object.
+ */
+class TestFunction extends Function {
+  TestFunction() {
+    this.getADecorator().(Name).getId() = "test" and
+    this.getPositionalParameterCount() >= 1
+  }
+
+  /** Gets the name of the timer parameter (first parameter). */
+  string getTimerParamName() { result = this.getArgName(0) }
+}
+
+/** Gets an IntegerLiteral from a timestamp expression (single int or tuple of ints). */
+private IntegerLiteral timestampLiteral(Expr timestamps) {
+  result = timestamps
+  or
+  result = timestamps.(Tuple).getAnElt()
+}
+
+/**
+ * Gets an element from a timestamp subscript index. Each element is either
+ * an `IntegerLiteral` (live), a `Call` to `dead` (dead), a `Name("never")`
+ * (never), or a tuple containing any mix of these.
+ */
+private Expr timestampElement(Expr timestamps) {
+  result = timestamps and not timestamps instanceof Tuple
+  or
+  result = timestamps.(Tuple).getAnElt()
+}
+
+/** Gets a live timestamp value from a subscript index expression. */
+private IntegerLiteral liveTimestampLiteral(Expr timestamps) {
+  result = timestampElement(timestamps) and
+  not result = any(Call c).getAnArg()
+}
+
+/** Gets a dead timestamp value from a subscript index expression. */
+private IntegerLiteral deadTimestampLiteral(Expr timestamps) {
+  exists(Call c |
+    c = timestampElement(timestamps) and
+    c.getFunc().(Name).getId() = "dead" and
+    result = c.getArg(0)
+  )
+}
+
+/** Holds if the subscript index contains `never`. */
+private predicate hasNever(Expr timestamps) {
+  timestampElement(timestamps).(Name).getId() = "never"
+}
+
+/** A timer annotation in the AST. */
+private newtype TTimerAnnotation =
+  /** `expr @ t[n]` or `expr @ t[n, m, ...]` or `expr @ t[dead(n), m, never]` */
+  TMatmulAnnotation(TestFunction func, Expr annotated, Expr timestamps) {
+    exists(BinaryExpr be |
+      be.getOp() instanceof MatMult and
+      be.getRight().(Subscript).getObject().(Name).getId() = func.getTimerParamName() and
+      be.getScope().getEnclosingScope*() = func and
+      annotated = be.getLeft() and
+      timestamps = be.getRight().(Subscript).getIndex()
+    )
+  } or
+  /** `t(expr, n)` */
+  TCallAnnotation(TestFunction func, Expr annotated, Expr timestamps) {
+    exists(Call call |
+      call.getFunc().(Name).getId() = func.getTimerParamName() and
+      call.getScope().getEnclosingScope*() = func and
+      annotated = call.getArg(0) and
+      timestamps = call.getArg(1)
+    )
+  }
+
+/** A timer annotation (wrapping the newtype for a clean API). */
+class TimerAnnotation extends TTimerAnnotation {
+  /** Gets a live timestamp value from this annotation. */
+  int getATimestamp() { exists(this.getTimestampExpr(result)) }
+
+  /** Gets the source expression for live timestamp value `ts`. */
+  IntegerLiteral getTimestampExpr(int ts) {
+    result = liveTimestampLiteral(this.getTimestampsExpr()) and
+    result.getValue() = ts
+  }
+
+  /** Gets a dead timestamp value from this annotation. */
+  int getADeadTimestamp() { exists(this.getDeadTimestampExpr(result)) }
+
+  /** Gets the source expression for dead timestamp value `ts`. */
+  IntegerLiteral getDeadTimestampExpr(int ts) {
+    result = deadTimestampLiteral(this.getTimestampsExpr()) and
+    result.getValue() = ts
+  }
+
+  /** Gets the raw timestamp expression (single element or tuple). */
+  abstract Expr getTimestampsExpr();
+
+  /** Gets the test function this annotation belongs to. */
+  abstract TestFunction getTestFunction();
+
+  /** Gets the annotated expression (the LHS of `@` or the first arg of `t(...)`). */
+  abstract Expr getAnnotatedExpr();
+
+  /** Gets the enclosing annotation expression (the `BinaryExpr` or `Call`). */
+  abstract Expr getTimerExpr();
+
+  /** Holds if timestamp `ts` is marked as dead in this annotation. */
+  predicate isDeadTimestamp(int ts) { ts = this.getADeadTimestamp() }
+
+  /** Holds if all timestamps in this annotation are dead (no live timestamps). */
+  predicate isDead() {
+    not exists(this.getATimestamp()) and
+    not this.isNever() and
+    exists(this.getADeadTimestamp())
+  }
+
+  /** Holds if this is a never-evaluated annotation (contains `never`). */
+  predicate isNever() { hasNever(this.getTimestampsExpr()) }
+
+  string toString() { result = this.getAnnotatedExpr().toString() }
+
+  Location getLocation() { result = this.getAnnotatedExpr().getLocation() }
+}
+
+/** A matmul-based timer annotation: `expr @ t[...]`. */
+class MatmulTimerAnnotation extends TMatmulAnnotation, TimerAnnotation {
+  TestFunction func;
+  Expr annotated;
+  Expr timestamps;
+
+  MatmulTimerAnnotation() { this = TMatmulAnnotation(func, annotated, timestamps) }
+
+  override Expr getTimestampsExpr() { result = timestamps }
+
+  override TestFunction getTestFunction() { result = func }
+
+  override Expr getAnnotatedExpr() { result = annotated }
+
+  override BinaryExpr getTimerExpr() { result.getLeft() = annotated }
+}
+
+/** A call-based timer annotation: `t(expr, n)`. */
+class CallTimerAnnotation extends TCallAnnotation, TimerAnnotation {
+  TestFunction func;
+  Expr annotated;
+  Expr timestamps;
+
+  CallTimerAnnotation() { this = TCallAnnotation(func, annotated, timestamps) }
+
+  override Expr getTimestampsExpr() { result = timestamps }
+
+  override TestFunction getTestFunction() { result = func }
+
+  override Expr getAnnotatedExpr() { result = annotated }
+
+  override Call getTimerExpr() { result.getArg(0) = annotated }
+}
+
+/**
+ * Signature module defining the CFG interface needed by evaluation-order tests.
+ * This allows the test utilities to be instantiated with different CFG implementations.
+ */
+signature module EvalOrderCfgSig {
+  /** A control flow node. */
+  class CfgNode {
+    /** Gets a textual representation of this node. */
+    string toString();
+
+    /** Gets the location of this node. */
+    Location getLocation();
+
+    /** Gets the AST node corresponding to this CFG node, if any. */
+    AstNode getNode();
+
+    /** Gets a successor of this CFG node (including exceptional). */
+    CfgNode getASuccessor();
+
+    /** Gets a true-branch successor of this CFG node, if any. */
+    CfgNode getATrueSuccessor();
+
+    /** Gets a false-branch successor of this CFG node, if any. */
+    CfgNode getAFalseSuccessor();
+
+    /** Gets an exceptional successor of this CFG node. */
+    CfgNode getAnExceptionalSuccessor();
+
+    /** Gets the scope containing this CFG node. */
+    Scope getScope();
+
+    /** Gets the basic block containing this CFG node. */
+    BasicBlock getBasicBlock();
+  }
+
+  /** A basic block in the control flow graph. */
+  class BasicBlock {
+    /** Gets the CFG node at position `n` in this basic block. */
+    CfgNode getNode(int n);
+
+    /** Holds if this basic block reaches `bb` (reflexive). */
+    predicate reaches(BasicBlock bb);
+
+    /** Holds if this basic block strictly reaches `bb` (non-reflexive). */
+    predicate strictlyReaches(BasicBlock bb);
+
+    /** Holds if this basic block strictly dominates `bb`. */
+    predicate strictlyDominates(BasicBlock bb);
+  }
+
+  /** Gets the entry CFG node for scope `s`. */
+  CfgNode scopeGetEntryNode(Scope s);
+}
+
+/**
+ * Parameterised module providing CFG-dependent utilities for evaluation-order tests.
+ * Instantiate with a specific CFG implementation to get `TimerCfgNode` and related predicates.
+ */
+module EvalOrderCfgUtils<EvalOrderCfgSig Input> {
+  /** The CFG node type from the underlying implementation. */
+  final class CfgNode = Input::CfgNode;
+
+  /** The basic block type from the underlying implementation (named to avoid clash with `python::BasicBlock`). */
+  final class CfgBasicBlock = Input::BasicBlock;
+
+  /** Gets the entry CFG node for scope `s`. */
+  CfgNode scopeGetEntryNode(Scope s) { result = Input::scopeGetEntryNode(s) }
+
+  /**
+   * A CFG node corresponding to a timer annotation.
+   */
+  class TimerCfgNode extends CfgNode {
+    private TimerAnnotation annot;
+
+    TimerCfgNode() { annot.getAnnotatedExpr() = this.getNode() }
+
+    /** Gets a timestamp value from this annotation. */
+    int getATimestamp() { result = annot.getATimestamp() }
+
+    /** Gets the source expression for timestamp value `ts`. */
+    IntegerLiteral getTimestampExpr(int ts) { result = annot.getTimestampExpr(ts) }
+
+    /** Gets the test function this annotation belongs to. */
+    TestFunction getTestFunction() { result = annot.getTestFunction() }
+
+    /** Holds if timestamp `ts` is marked as dead. */
+    predicate isDeadTimestamp(int ts) { annot.isDeadTimestamp(ts) }
+
+    /** Holds if all timestamps in this annotation are dead. */
+    predicate isDead() { annot.isDead() }
+
+    /** Holds if this is a never-evaluated annotation. */
+    predicate isNever() { annot.isNever() }
+  }
+
+  /**
+   * Holds if `next` is the next timer annotation reachable from `n` via
+   * CFG successors (both normal and exceptional), skipping non-annotated
+   * intermediaries within the same scope.
+   */
+  predicate nextTimerAnnotation(CfgNode n, TimerCfgNode next) {
+    next = n.getASuccessor() and
+    next.getScope() = n.getScope()
+    or
+    exists(CfgNode mid |
+      mid = n.getASuccessor() and
+      not mid instanceof TimerCfgNode and
+      mid.getScope() = n.getScope() and
+      nextTimerAnnotation(mid, next)
+    )
+  }
+
+  /**
+   * Holds if `next` is the next timer annotation reachable from `n` via
+   * the true branch, skipping non-annotated intermediaries and after-value
+   * nodes for the same AST node.
+   */
+  predicate nextTimerAnnotationFromTrue(CfgNode n, TimerCfgNode next) {
+    exists(CfgNode trueSucc |
+      trueSucc = n.getATrueSuccessor() and
+      trueSucc.getScope() = n.getScope()
+    |
+      // If the true successor is a different annotated node, use it
+      next = trueSucc and next.getNode() != n.getNode()
+      or
+      // Otherwise skip through it (it's an after-value node for the same expr)
+      nextTimerAnnotation(trueSucc, next)
+    )
+  }
+
+  /**
+   * Holds if `next` is the next timer annotation reachable from `n` via
+   * the false branch, skipping non-annotated intermediaries and after-value
+   * nodes for the same AST node.
+   */
+  predicate nextTimerAnnotationFromFalse(CfgNode n, TimerCfgNode next) {
+    exists(CfgNode falseSucc |
+      falseSucc = n.getAFalseSuccessor() and
+      falseSucc.getScope() = n.getScope()
+    |
+      // If the false successor is a different annotated node, use it
+      next = falseSucc and next.getNode() != n.getNode()
+      or
+      // Otherwise skip through it (it's an after-value node for the same expr)
+      nextTimerAnnotation(falseSucc, next)
+    )
+  }
+
+  /** CFG-dependent test predicates, one per evaluation-order query. */
+  module CfgTests {
+    /**
+     * Holds if live annotation `a` in function `f` is unreachable from
+     * the function entry in the CFG.
+     */
+    predicate allLiveReachable(TimerCfgNode a, TestFunction f) {
+      not a.isDead() and
+      f = a.getTestFunction() and
+      a.getScope() = f and
+      not scopeGetEntryNode(f).getBasicBlock().reaches(a.getBasicBlock())
+    }
+
+    /**
+     * Holds if annotated node `a` is followed by unannotated `succ` in the
+     * same basic block.
+     */
+    predicate basicBlockAnnotationGap(TimerCfgNode a, CfgNode succ) {
+      exists(CfgBasicBlock bb, int i |
+        a = bb.getNode(i) and
+        succ = bb.getNode(i + 1)
+      ) and
+      not succ instanceof TimerCfgNode and
+      not isUnannotatable(succ.getNode()) and
+      not isTimerMechanism(succ.getNode(), a.getTestFunction()) and
+      not exists(a.getAnExceptionalSuccessor()) and
+      succ.getNode() instanceof Expr
+    }
+
+    /**
+     * Holds if annotations `a` and `b` appear in the same basic block with
+     * `a` before `b`, but `a`'s minimum timestamp is not less than `b`'s.
+     */
+    predicate basicBlockOrdering(TimerCfgNode a, TimerCfgNode b, int minA, int minB) {
+      exists(CfgBasicBlock bb, int i, int j | a = bb.getNode(i) and b = bb.getNode(j) and i < j) and
+      minA = min(a.getATimestamp()) and
+      minB = min(b.getATimestamp()) and
+      minA >= minB
+    }
+
+    /**
+     * Holds if function `f` has an annotation in a nested scope
+     * (generator, async function, comprehension, lambda).
+     */
+    private predicate hasNestedScopeAnnotation(TestFunction f) {
+      exists(TimerAnnotation a |
+        a.getTestFunction() = f and
+        a.getAnnotatedExpr().getScope() != f
+      )
+    }
+
+    /**
+     * Holds if annotation `ann` with timestamp `a` has no consecutive
+     * successor (expected `a + 1`) in the CFG.
+     */
+    predicate consecutiveTimestamps(TimerAnnotation ann, int a) {
+      not hasNestedScopeAnnotation(ann.getTestFunction()) and
+      not ann.isDead() and
+      a = ann.getATimestamp() and
+      not exists(TimerCfgNode x, TimerCfgNode y |
+        ann.getAnnotatedExpr() = x.getNode() and
+        nextTimerAnnotation(x, y) and
+        (a + 1) = y.getATimestamp()
+      ) and
+      // Exclude the maximum timestamp in the function (it has no successor)
+      not a =
+        max(TimerAnnotation other |
+          other.getTestFunction() = ann.getTestFunction()
+        |
+          other.getATimestamp()
+        )
+    }
+
+    /**
+     * Holds if the expression annotated with `t.never` is reachable from
+     * its scope's entry.
+     */
+    predicate neverReachable(TimerAnnotation ann) {
+      ann.isNever() and
+      exists(CfgNode n, Scope s |
+        n.getNode() = ann.getAnnotatedExpr() and
+        s = n.getScope() and
+        (
+          // Reachable via inter-block path (includes same block)
+          scopeGetEntryNode(s).getBasicBlock().reaches(n.getBasicBlock())
+          or
+          // In same block as entry but at a later index
+          exists(CfgBasicBlock bb, int i, int j |
+            bb.getNode(i) = scopeGetEntryNode(s) and bb.getNode(j) = n and i < j
+          )
+        )
+      )
+    }
+
+    /**
+     * Holds if consecutive annotated nodes `a` -> `b` have backward time
+     * flow (`minA >= maxB`).
+     */
+    predicate noBackwardFlow(TimerCfgNode a, TimerCfgNode b, int minA, int maxB) {
+      nextTimerAnnotation(a, b) and
+      not a.isDead() and
+      not b.isDead() and
+      minA = min(a.getATimestamp()) and
+      maxB = max(b.getATimestamp()) and
+      minA >= maxB
+    }
+
+    /**
+     * Holds if annotations `a` and `b` share timestamp `ts` but `a`
+     * can reach `b` in the CFG.
+     */
+    predicate noSharedReachable(TimerCfgNode a, TimerCfgNode b, int ts) {
+      a != b and
+      not a.isDead() and
+      not b.isDead() and
+      a.getTestFunction() = b.getTestFunction() and
+      ts = a.getATimestamp() and
+      ts = b.getATimestamp() and
+      (
+        a.getBasicBlock().strictlyReaches(b.getBasicBlock())
+        or
+        exists(CfgBasicBlock bb, int i, int j | a = bb.getNode(i) and b = bb.getNode(j) and i < j)
+      )
+    }
+
+    /**
+     * Holds if consecutive single-timestamp annotations `a` -> `b` on a
+     * forward edge have `maxA >= minB`.
+     */
+    predicate strictForward(TimerCfgNode a, TimerCfgNode b, int maxA, int minB) {
+      nextTimerAnnotation(a, b) and
+      not a.isDead() and
+      not b.isDead() and
+      // Only apply to non-loop code (single timestamps on both sides)
+      strictcount(a.getATimestamp()) = 1 and
+      strictcount(b.getATimestamp()) = 1 and
+      // Forward edge: B does not strictly dominate A (excludes loop back-edges
+      // but still checks same-basic-block pairs)
+      not b.getBasicBlock().strictlyDominates(a.getBasicBlock()) and
+      maxA = max(a.getATimestamp()) and
+      minB = min(b.getATimestamp()) and
+      maxA >= minB
+    }
+
+    /**
+     * Holds if CFG node `n` in test function `f` does not belong to any basic block.
+     */
+    predicate noBasicBlock(CfgNode n, TestFunction f) {
+      n.getScope() = f and
+      not exists(n.getBasicBlock())
+    }
+
+    /**
+     * Holds if non-dead annotation `ann` has no corresponding CFG node.
+     */
+    predicate annotationWithoutCfgNode(TimerAnnotation ann) {
+      not ann.isDead() and
+      not ann.isNever() and
+      not exists(CfgNode n | n.getNode() = ann.getAnnotatedExpr())
+    }
+
+    predicate annotationWithCfgNode(TimerAnnotation ann) {
+      exists(CfgNode n | n.getNode() = ann.getAnnotatedExpr())
+    }
+
+    /**
+     * Holds if annotation `ann` with timestamp `a` has no consecutive
+     * predecessor (expected `a - 1`) in the CFG.
+     */
+    predicate consecutivePredecessorTimestamps(TimerAnnotation ann, int a) {
+      not hasNestedScopeAnnotation(ann.getTestFunction()) and
+      not ann.isDead() and
+      a = ann.getATimestamp() and
+      not exists(TimerCfgNode x, TimerCfgNode y |
+        ann.getAnnotatedExpr() = y.getNode() and
+        nextTimerAnnotation(x, y) and
+        (a - 1) = x.getATimestamp()
+      ) and
+      // Exclude the minimum timestamp in the function (it has no predecessor)
+      not a =
+        min(TimerAnnotation other |
+          other.getTestFunction() = ann.getTestFunction() and
+          not other.isDead()
+        |
+          other.getATimestamp()
+        )
+    }
+
+    /**
+     * Holds if `node` has both a true and false successor, but the true
+     * successor's timestamp `ts` is not marked as dead on the false
+     * successor (or vice versa).
+     *
+     * This checks that boolean branches are properly annotated: when a
+     * condition splits into true/false paths, the next annotated node
+     * on each side should account for the other side's timestamps as dead.
+     */
+    predicate missingBranchTimestamp(TimerCfgNode node, int ts, string branch) {
+      not hasNestedScopeAnnotation(node.getTestFunction()) and
+      exists(TimerCfgNode trueNext, TimerCfgNode falseNext |
+        nextTimerAnnotationFromTrue(node, trueNext) and
+        nextTimerAnnotationFromFalse(node, falseNext) and
+        trueNext != falseNext
+      |
+        // True successor has live timestamp ts, but false successor
+        // doesn't have it as dead
+        ts = trueNext.getATimestamp() and
+        not falseNext.isDeadTimestamp(ts) and
+        not ts = falseNext.getATimestamp() and
+        branch = "false"
+        or
+        // False successor has live timestamp ts, but true successor
+        // doesn't have it as dead
+        ts = falseNext.getATimestamp() and
+        not trueNext.isDeadTimestamp(ts) and
+        not ts = trueNext.getATimestamp() and
+        branch = "true"
+      )
+    }
+  }
+}
+
+/**
+ * Holds if `e` is part of the timer mechanism: a top-level timer
+ * expression or a (transitive) sub-expression of one.
+ */
+predicate isTimerMechanism(Expr e, TestFunction f) {
+  exists(TimerAnnotation a |
+    a.getTestFunction() = f and
+    e = a.getTimerExpr().getASubExpression*()
+  )
+}
+
+/**
+ * Holds if expression `e` cannot be annotated due to Python syntax
+ * limitations (e.g., it is a definition target, a pattern, or part
+ * of a decorator application).
+ */
+predicate isUnannotatable(Expr e) {
+  // Function/class definitions
+  e instanceof FunctionExpr
+  or
+  e instanceof ClassExpr
+  or
+  // Docstrings are string literals used as expression statements
+  e instanceof StringLiteral and e.getParent() instanceof ExprStmt
+  or
+  // Function parameters are bound by the call, not evaluated in the body
+  e instanceof Parameter
+  or
+  // Name nodes that are definitions or deletions (assignment targets, def/class
+  // name bindings, augmented assignment targets, for-loop targets, del targets)
+  e.(Name).isDefinition()
+  or
+  e.(Name).isDeletion()
+  or
+  // Tuple/List/Starred nodes in assignment or for-loop targets are
+  // structural unpack patterns, not evaluations
+  (e instanceof Tuple or e instanceof List or e instanceof Starred) and
+  e = any(AssignStmt a).getATarget().getASubExpression*()
+  or
+  (e instanceof Tuple or e instanceof List or e instanceof Starred) and
+  e = any(For f).getTarget().getASubExpression*()
+  or
+  // The decorator call node wrapping a function/class definition,
+  // and its sub-expressions (the decorator name itself)
+  e = any(FunctionExpr func).getADecoratorCall().getASubExpression*()
+  or
+  e = any(ClassExpr cls).getADecoratorCall().getASubExpression*()
+  or
+  // Augmented assignment (x += e): the implicit BinaryExpr for the operation
+  e = any(AugAssign aug).getOperation()
+  or
+  // with-statement `as` variables are bindings
+  (e instanceof Name or e instanceof Tuple or e instanceof List) and
+  e = any(With w).getOptionalVars().getASubExpression*()
+  or
+  // except-clause exception type and `as` variable are part of except syntax
+  exists(ExceptStmt ex | e = ex.getType() or e = ex.getName())
+  or
+  // match/case pattern expressions are part of pattern syntax
+  e.getParent+() instanceof Pattern
+  or
+  // Subscript/Attribute nodes on the LHS of an assignment are store
+  // operations, not value expressions (including nested ones like d["a"][1])
+  (e instanceof Subscript or e instanceof Attribute) and
+  e = any(AssignStmt a).getATarget().getASubExpression*()
+  or
+  // Match/case guard nodes are part of case syntax
+  e instanceof Guard
+  or
+  // Yield/YieldFrom in statement position — the return value is
+  // discarded and cannot be meaningfully annotated
+  (e instanceof Yield or e instanceof YieldFrom) and
+  e.getParent() instanceof ExprStmt
+  or
+  // Synthetic nodes inside desugared comprehensions
+  e.getScope() = any(Comp c).getFunction() and
+  (
+    e.(Name).getId() = ".0"
+    or
+    e instanceof Tuple and e.getParent() instanceof Yield
+  )
+}
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py
new file mode 100644
index 000000000000..692a9c6e407c
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_assert_raise.py
@@ -0,0 +1,56 @@
+"""Assert and raise statement evaluation order."""
+
+from timer import test, dead
+
+
+@test
+def test_assert_true(t):
+    x = True @ t[0]
+    assert x @ t[1]
+    y = 1 @ t[2]
+
+
+@test
+def test_assert_true_with_message(t):
+    x = True @ t[0]
+    assert x @ t[1], "msg" @ t[dead(2)]
+    y = 1 @ t[2]
+
+
+@test
+def test_assert_false_caught(t):
+    try:
+        x = False @ t[0]
+        assert x @ t[1], "fail" @ t[2]
+    except AssertionError:
+        y = 1 @ t[3]
+
+
+@test
+def test_raise_caught(t):
+    try:
+        x = 1 @ t[0]
+        raise ((ValueError @ t[1])("test" @ t[2]) @ t[3])
+    except ValueError:
+        y = 2 @ t[4]
+
+
+@test
+def test_raise_from_caught(t):
+    try:
+        x = 1 @ t[0]
+        raise ((ValueError @ t[1])("test" @ t[2]) @ t[3]) from ((RuntimeError @ t[4])("cause" @ t[5]) @ t[6])
+    except ValueError:
+        y = 2 @ t[7]
+
+
+@test
+def test_bare_reraise(t):
+    try:
+        try:
+            raise ((ValueError @ t[0])("test" @ t[1]) @ t[2])
+        except ValueError:
+            x = 1 @ t[3]
+            raise
+    except ValueError:
+        y = 2 @ t[4]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_async.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_async.py
new file mode 100644
index 000000000000..0c9b08e3e9eb
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_async.py
@@ -0,0 +1,97 @@
+"""Async/await evaluation order tests.
+
+Coroutine bodies are lazy — like generators, the body runs only when
+awaited (or driven by the event loop).  asyncio.run() drives the
+coroutine to completion synchronously from the caller's perspective.
+"""
+
+import asyncio
+from contextlib import asynccontextmanager
+from timer import test
+
+
+@test
+def test_simple_async(t):
+    """Simple async function: body runs inside asyncio.run()."""
+    async def coro():
+        x = 1 @ t[4]
+        return x @ t[5]
+
+    result = ((asyncio @ t[0]).run @ t[1])((coro @ t[2])() @ t[3]) @ t[6]
+
+
+@test
+def test_await_expression(t):
+    """await suspends the caller until the inner coroutine completes."""
+    async def helper():
+        return 1 @ t[4]
+
+    async def main():
+        x = await helper() @ t[5]
+        return x @ t[6]
+
+    result = ((asyncio @ t[0]).run @ t[1])((main @ t[2])() @ t[3]) @ t[7]
+
+
+@test
+def test_async_for(t):
+    """async for iterates an async generator."""
+    async def agen():
+        yield 1 @ t[5]
+        yield 2 @ t[7]
+
+    async def main():
+        async for val in agen() @ t[4]:
+            val @ t[6, 8]
+
+    ((asyncio @ t[0]).run @ t[1])((main @ t[2])() @ t[3]) @ t[9]
+
+
+@test
+def test_async_with(t):
+    """async with enters/exits an async context manager."""
+    @asynccontextmanager
+    async def ctx():
+        yield 1 @ t[5]
+
+    async def main():
+        async with ctx() @ t[4] as val:
+            val @ t[6]
+
+    ((asyncio @ t[0]).run @ t[1])((main @ t[2])() @ t[3]) @ t[7]
+
+
+@test
+def test_multiple_awaits(t):
+    """Sequential awaits in one coroutine."""
+    async def task_a():
+        return 10 @ t[4]
+
+    async def task_b():
+        return 20 @ t[6]
+
+    async def main():
+        a = await task_a() @ t[5]
+        b = await task_b() @ t[7]
+        return (a @ t[8] + b @ t[9]) @ t[10]
+
+    result = ((asyncio @ t[0]).run @ t[1])((main @ t[2])() @ t[3]) @ t[11]
+
+
+@test
+def test_gather(t):
+    """asyncio.gather schedules coroutines as concurrent tasks."""
+    async def task_a():
+        return 1 @ t[6]
+
+    async def task_b():
+        return 2 @ t[7]
+
+    async def main():
+        results = await asyncio.gather(
+            task_a() @ t[4],
+            task_b() @ t[5],
+        ) @ t[8]
+        return results @ t[9]
+
+    result = ((asyncio @ t[0]).run @ t[1])((main @ t[2])() @ t[3]) @ t[10]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_augassign.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_augassign.py
new file mode 100644
index 000000000000..2f1d5eb5c3e6
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_augassign.py
@@ -0,0 +1,53 @@
+"""Augmented assignment evaluation order."""
+
+from timer import test
+
+
+@test
+def test_plus_equals(t):
+    x = 1 @ t[0]
+    x += 2 @ t[1]
+    y = x @ t[2]
+
+
+@test
+def test_sub_mul_div(t):
+    x = 20 @ t[0]
+    x -= 5 @ t[1]
+    x *= 2 @ t[2]
+    x /= 6 @ t[3]
+    x = 17 @ t[4]
+    x //= 3 @ t[5]
+    x %= 3 @ t[6]
+    y = x @ t[7]
+
+
+@test
+def test_power_equals(t):
+    x = 2 @ t[0]
+    x **= 3 @ t[1]
+    y = x @ t[2]
+
+
+@test
+def test_bitwise_equals(t):
+    x = 0b1111 @ t[0]
+    x &= 0b1010 @ t[1]
+    x |= 0b0101 @ t[2]
+    x ^= 0b0011 @ t[3]
+    y = x @ t[4]
+
+
+@test
+def test_shift_equals(t):
+    x = 1 @ t[0]
+    x <<= 4 @ t[1]
+    x >>= 2 @ t[2]
+    y = x @ t[3]
+
+
+@test
+def test_list_extend(t):
+    x = [1 @ t[0], 2 @ t[1]] @ t[2]
+    x += [3 @ t[3], 4 @ t[4]] @ t[5]
+    y = x @ t[6]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py
new file mode 100644
index 000000000000..3e8ee925d913
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_basic.py
@@ -0,0 +1,223 @@
+"""Basic expression evaluation order.
+
+These tests verify that sub-expressions within a single expression
+are evaluated in the expected order (typically left to right for
+operands of binary operators, elements of collection literals, etc.)
+
+Every evaluated expression has a timestamp annotation, except the
+timer mechanism itself (t[n], t.dead[n]).
+"""
+
+from timer import test, never
+
+
+@test
+def test_sequential_statements(t):
+    """Statements execute top to bottom."""
+    x = 1 @ t[0]
+    y = 2 @ t[1]
+    z = 3 @ t[2]
+
+
+@test
+def test_binary_add(t):
+    """In a + b, left operand evaluates before right."""
+    x = (1 @ t[0] + 2 @ t[1]) @ t[2]
+
+
+@test
+def test_binary_subtract(t):
+    """In a - b, left operand evaluates before right."""
+    x = (10 @ t[0] - 3 @ t[1]) @ t[2]
+
+
+@test
+def test_binary_multiply(t):
+    """In a * b, left operand evaluates before right."""
+    x = ((3 @ t[0]) * (4 @ t[1])) @ t[2]
+
+
+@test
+def test_nested_binary(t):
+    """Sub-expressions evaluate before their containing expression."""
+    x = ((1 @ t[0] + 2 @ t[1]) @ t[2] + (3 @ t[3] + 4 @ t[4]) @ t[5]) @ t[6]
+
+
+@test
+def test_chained_add(t):
+    """a + b + c is (a + b) + c: left to right."""
+    x = ((1 @ t[0] + 2 @ t[1]) @ t[2] + 3 @ t[3]) @ t[4]
+
+
+@test
+def test_mixed_precedence(t):
+    """In a + b * c, all operands still evaluate left to right."""
+    x = (1 @ t[0] + ((2 @ t[1]) * (3 @ t[2])) @ t[3]) @ t[4]
+
+
+@test
+def test_string_concat(t):
+    """String concatenation operands: left to right."""
+    x = (("hello" @ t[0] + " " @ t[1]) @ t[2] + "world" @ t[3]) @ t[4]
+
+
+@test
+def test_comparison(t):
+    """In a < b, left operand evaluates before right."""
+    x = (1 @ t[0] < 2 @ t[1]) @ t[2]
+
+
+@test
+def test_chained_comparison(t):
+    """Chained a < b < c: all evaluated left to right (b only once)."""
+    x = (1 @ t[0] < 2 @ t[1] < 3 @ t[2]) @ t[3]
+
+
+@test
+def test_list_elements(t):
+    """List elements evaluate left to right."""
+    x = [1 @ t[0], 2 @ t[1], 3 @ t[2]] @ t[3]
+
+
+@test
+def test_dict_entries(t):
+    """Dict: key before value, entries left to right."""
+    d = {1 @ t[0]: "a" @ t[1], 2 @ t[2]: "b" @ t[3]} @ t[4]
+
+
+@test
+def test_tuple_elements(t):
+    """Tuple elements evaluate left to right."""
+    x = (1 @ t[0], 2 @ t[1], 3 @ t[2]) @ t[3]
+
+
+@test
+def test_set_elements(t):
+    """Set elements evaluate left to right."""
+    x = {1 @ t[0], 2 @ t[1], 3 @ t[2]} @ t[3]
+
+
+@test
+def test_subscript(t):
+    """In obj[idx], object evaluates before index."""
+    x = ([10 @ t[0], 20 @ t[1], 30 @ t[2]] @ t[3])[1 @ t[4]] @ t[5]
+
+
+@test
+def test_slice(t):
+    """Slice parameters: object, then start, then stop."""
+    x = ([1 @ t[0], 2 @ t[1], 3 @ t[2], 4 @ t[3], 5 @ t[4]] @ t[5])[1 @ t[6]:3 @ t[7]] @ t[8]
+
+
+@test
+def test_method_call(t):
+    """Object evaluated, then attribute lookup, then arguments left to right, then call."""
+    x = (("hello world" @ t[0]).replace @ t[1])("world" @ t[2], "there" @ t[3]) @ t[4]
+
+
+@test
+def test_method_chaining(t):
+    """Chained method calls: left to right."""
+    x = ((((" hello " @ t[0]).strip @ t[1])() @ t[2]).upper @ t[3])() @ t[4]
+
+
+@test
+def test_unary_not(t):
+    """Unary not: operand evaluated first."""
+    x = (not True @ t[0]) @ t[1]
+
+
+@test
+def test_unary_neg(t):
+    """Unary negation: operand evaluated first."""
+    x = (-(3 @ t[0])) @ t[1]
+
+
+@test
+def test_multiple_assignment(t):
+    """RHS evaluated once in x = y = expr."""
+    x = y = (1 @ t[0] + 2 @ t[1]) @ t[2]
+
+
+@test
+def test_callable_syntax(t):
+    """t(value, n) is equivalent to value @ t[n]."""
+    x = (1 @ t[0] + 2 @ t[1]) @ t[2]
+    y = (x @ t[3] * 3 @ t[4]) @ t[5]
+
+
+@test
+def test_subscript_assign(t):
+    """In obj[idx] = val, value is evaluated before target sub-expressions."""
+    lst = [0 @ t[0], 0 @ t[1], 0 @ t[2]] @ t[3]
+    (lst @ t[5])[1 @ t[6]] = 42 @ t[4]
+    x = lst @ t[7]
+
+
+@test
+def test_attribute_assign(t):
+    """In obj.attr = val, value is evaluated before the object."""
+    class Obj:
+        pass
+    o = (Obj @ t[0])() @ t[1]
+    (o @ t[3]).x = 42 @ t[2]
+    y = (o @ t[4]).x @ t[5]
+
+
+@test
+def test_nested_subscript_assign(t):
+    """Nested subscript assignment: val, then outer obj, then keys."""
+    d = {"a" @ t[0]: [0 @ t[1], 0 @ t[2]] @ t[3]} @ t[4]
+    (d @ t[6])["a" @ t[7]][1 @ t[8]] = 99 @ t[5]
+    x = d @ t[9]
+
+
+@test
+def test_unreachable_after_return(t):
+    """Code after return has no CFG node."""
+    def f():
+        x = 1 @ t[1]
+        return x @ t[2]
+        y = 2 @ t[never]
+    result = (f @ t[0])() @ t[3]
+
+
+@test
+def test_none_literal(t):
+    """None is a name constant."""
+    x = None @ t[0]
+    y = (x @ t[1] is None @ t[2]) @ t[3]
+
+
+@test
+def test_delete(t):
+    """del statement removes a variable binding."""
+    x = 1 @ t[0]
+    del x
+    y = 2 @ t[1]
+
+
+@test
+def test_global(t):
+    """global statement allows writing to module-level variable."""
+    global _test_global_var
+    _test_global_var = 1 @ t[0]
+    x = _test_global_var @ t[1]
+
+
+@test
+def test_nonlocal(t):
+    """nonlocal statement allows inner function to rebind outer variable."""
+    x = 0 @ t[0]
+    def inner():
+        nonlocal x
+        x = 1 @ t[2]
+    (inner @ t[1])() @ t[3]
+    y = x @ t[4]
+
+
+@test
+def test_walrus(t):
+    """Walrus operator := evaluates the RHS and binds it."""
+    if (y := 1 @ t[0]) @ t[1]:
+        z = y @ t[2]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py
new file mode 100644
index 000000000000..a3b2268a8315
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_boolean.py
@@ -0,0 +1,76 @@
+"""Short-circuit boolean operators and evaluation order."""
+
+from timer import test, dead
+
+
+@test
+def test_and_both_sides(t):
+    # True and X — both operands evaluated, result is X
+    x = (True @ t[0] and 42 @ t[1, dead(2)]) @ t[dead(1), 2]
+
+
+@test
+def test_and_short_circuit(t):
+    # False and ... — right side never evaluated
+    x = (False @ t[0] and True @ t[dead(1)]) @ t[1, dead(2)]
+
+
+@test
+def test_or_short_circuit(t):
+    # True or ... — right side never evaluated
+    x = (True @ t[0] or False @ t[dead(1)]) @ t[1, dead(2)]
+
+
+@test
+def test_or_both_sides(t):
+    # False or X — both operands evaluated, result is X
+    x = (False @ t[0] or 42 @ t[1, dead(2)]) @ t[dead(1), 2]
+
+
+@test
+def test_not(t):
+    # not evaluates its operand, then negates
+    x = (not True @ t[0]) @ t[1]
+    y = (not False @ t[2]) @ t[3]
+
+
+@test
+def test_chained_and(t):
+    # 1 and 2 and 3 — all truthy, all evaluated left-to-right
+    x = (1 @ t[0] and 2 @ t[1, dead(3)] and 3 @ t[2, dead(3)]) @ t[dead(1), dead(2), 3]
+
+
+@test
+def test_chained_or(t):
+    # 0 or "" or 42 — first two falsy, all evaluated until truthy found
+    x = (0 @ t[0] or "" @ t[1, dead(3)] or 42 @ t[2, dead(3)]) @ t[dead(1), dead(2), 3]
+
+
+@test
+def test_mixed_and_or(t):
+    # True and False or 42 => (True and False) or 42 => False or 42 => 42
+    x = ((True @ t[0] and False @ t[1, dead(2)]) @ t[dead(1), 2, dead(4)] or 42 @ t[3, dead(4)]) @ t[dead(2), dead(3), 4]
+
+
+@test
+def test_and_side_effects(t):
+    # Both functions called when left side is truthy
+    def f():
+        return 10 @ t[1]
+
+    def g():
+        return 20 @ t[4]
+
+    x = ((f @ t[0])() @ t[2] and (g @ t[3])() @ t[5]) @ t[6]
+
+
+@test
+def test_or_side_effects(t):
+    # Both functions called when left side is falsy
+    def f():
+        return 0 @ t[1]
+
+    def g():
+        return 20 @ t[4]
+
+    x = ((f @ t[0])() @ t[2] or (g @ t[3])() @ t[5]) @ t[6]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_classes.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_classes.py
new file mode 100644
index 000000000000..92313b5073c3
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_classes.py
@@ -0,0 +1,74 @@
+"""Class definitions — evaluation order."""
+
+from timer import test
+
+
+@test
+def test_simple_class(t):
+    """Simple class definition and instantiation."""
+    class Foo:
+        pass
+    obj = (Foo @ t[0])() @ t[1]
+
+
+@test
+def test_class_with_bases(t):
+    """Base class expressions evaluated at class definition time."""
+    class Base:
+        pass
+    class Derived(Base @ t[0]):
+        pass
+    obj = (Derived @ t[1])() @ t[2]
+
+
+@test
+def test_class_with_methods(t):
+    """Object evaluated before method is called."""
+    class Foo:
+        def greet(self, name):
+            return ("hello " @ t[5] + name @ t[6]) @ t[7]
+    obj = (Foo @ t[0])() @ t[1]
+    msg = ((obj @ t[2]).greet @ t[3])("world" @ t[4]) @ t[8]
+
+
+@test
+def test_class_instantiation(t):
+    """Arguments to __init__ evaluate before instantiation completes."""
+    class Foo:
+        def __init__(self, x):
+            (self @ t[3]).x = x @ t[2]
+    obj = (Foo @ t[0])(42 @ t[1]) @ t[4]
+    val = (obj @ t[5]).x @ t[6]
+
+
+@test
+def test_method_call(t):
+    """Method arguments evaluate left-to-right before the call."""
+    class Calculator:
+        def __init__(self, value):
+            (self @ t[3]).value = value @ t[2]
+        def add(self, x):
+            return ((self @ t[8]).value @ t[9] + x @ t[10]) @ t[11]
+    calc = (Calculator @ t[0])(10 @ t[1]) @ t[4]
+    result = ((calc @ t[5]).add @ t[6])(5 @ t[7]) @ t[12]
+
+
+@test
+def test_class_level_attribute(t):
+    """Multiple attribute accesses in a single expression."""
+    class Config:
+        debug = True @ t[0]
+        version = 1 @ t[1]
+    x = ((Config @ t[2]).debug @ t[3], (Config @ t[4]).version @ t[5]) @ t[6]
+
+
+@test
+def test_class_decorator(t):
+    """Decorator expression evaluated, class defined, then decorator called."""
+    def add_marker(cls):
+        (cls @ t[2]).marked = True @ t[1]
+        return cls @ t[3]
+    @(add_marker @ t[0])
+    class Foo:
+        pass
+    result = (Foo @ t[4]).marked @ t[5]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_comprehensions.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_comprehensions.py
new file mode 100644
index 000000000000..8ce8ca6e4c46
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_comprehensions.py
@@ -0,0 +1,46 @@
+"""Evaluation order tests for comprehensions and generator expressions."""
+
+from timer import test
+
+
+@test
+def test_list_comprehension(t):
+    items = [1 @ t[0], 2 @ t[1], 3 @ t[2]] @ t[3]
+    result = [x @ t[5, 6, 7] for x in items @ t[4]] @ t[8]
+
+
+@test
+def test_filtered_comprehension(t):
+    items = [1 @ t[0], 2 @ t[1], 3 @ t[2], 4 @ t[3]] @ t[4]
+    result = [x @ t[14, 23] for x in items @ t[5] if (x @ t[6, 10, 15, 19] % 2 @ t[7, 11, 16, 20] == 0 @ t[8, 12, 17, 21]) @ t[9, 13, 18, 22]] @ t[24]
+
+
+@test
+def test_dict_comprehension(t):
+    items = [("a" @ t[0], 1 @ t[1]) @ t[2], ("b" @ t[3], 2 @ t[4]) @ t[5]] @ t[6]
+    result = {k @ t[8, 10]: v @ t[9, 11] for k, v in items @ t[7]} @ t[12]
+
+
+@test
+def test_set_comprehension(t):
+    items = [1 @ t[0], 2 @ t[1], 3 @ t[2]] @ t[3]
+    result = {x @ t[5, 6, 7] for x in items @ t[4]} @ t[8]
+
+
+@test
+def test_generator_expression(t):
+    items = [1 @ t[0], 2 @ t[1], 3 @ t[2]] @ t[3]
+    gen = (x @ t[8, 9, 10] for x in items @ t[4]) @ t[5]
+    result = (list @ t[6])(gen @ t[7]) @ t[11]
+
+
+@test
+def test_nested_comprehension(t):
+    matrix = [[1 @ t[0], 2 @ t[1]] @ t[2], [3 @ t[3], 4 @ t[4]] @ t[5]] @ t[6]
+    result = [x @ t[9, 10, 12, 13] for row in matrix @ t[7] for x in row @ t[8, 11]] @ t[14]
+
+
+@test
+def test_comprehension_with_call(t):
+    items = [1 @ t[0], 2 @ t[1], 3 @ t[2]] @ t[3]
+    result = [(str @ t[5, 8, 11])(x @ t[6, 9, 12]) @ t[7, 10, 13] for x in items @ t[4]] @ t[14]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py
new file mode 100644
index 000000000000..48d45a779583
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_conditional.py
@@ -0,0 +1,44 @@
+"""Ternary conditional expressions and evaluation order."""
+
+from timer import test, dead
+
+
+@test
+def test_ternary_true(t):
+    # Condition is True — consequent evaluated, alternative skipped
+    x = (1 @ t[1] if True @ t[0] else 2 @ t[dead(1)]) @ t[2]
+
+
+@test
+def test_ternary_false(t):
+    # Condition is False — alternative evaluated, consequent skipped
+    x = (1 @ t[dead(1)] if False @ t[0] else 2 @ t[1]) @ t[2]
+
+
+@test
+def test_ternary_nested(t):
+    # Nested: outer condition True, inner condition True
+    # ((10 if C1 else 20) if C2 else 30) — C2 first, then C1, then 10
+    x = ((10 @ t[2] if True @ t[1] else 20 @ t[dead(2)]) @ t[3] if True @ t[0] else 30 @ t[dead(1)]) @ t[4]
+
+
+@test
+def test_ternary_assignment(t):
+    # Ternary result assigned, then used in later expression
+    value = (100 @ t[1] if True @ t[0] else 200 @ t[dead(1)]) @ t[2]
+    result = (value @ t[3] + 1 @ t[4]) @ t[5]
+
+
+@test
+def test_ternary_complex_expressions(t):
+    # Complex sub-expressions in condition and consequent
+    x = ((1 @ t[3] + 2 @ t[4]) @ t[5] if (3 @ t[0] > 2 @ t[1]) @ t[2] else (4 @ t[dead(3)] + 5 @ t[dead(4)]) @ t[dead(5)]) @ t[6]
+
+
+@test
+def test_ternary_as_argument(t):
+    # Ternary used as a function argument
+    def f(a):
+        return a @ t[4]
+
+    result = (f @ t[0])((1 @ t[2] if True @ t[1] else 2 @ t[dead(2)]) @ t[3]) @ t[5]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_fstring.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_fstring.py
new file mode 100644
index 000000000000..2dd36f6ef36a
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_fstring.py
@@ -0,0 +1,34 @@
+"""F-string evaluation order."""
+
+from timer import test
+
+
+@test
+def test_simple_fstring(t):
+    name = "world" @ t[0]
+    s = f"hello {name @ t[1]}" @ t[2]
+
+
+@test
+def test_multi_expr_fstring(t):
+    a = "hello" @ t[0]
+    b = "world" @ t[1]
+    s = f"{a @ t[2]} {b @ t[3]}" @ t[4]
+
+
+@test
+def test_nested_fstring(t):
+    inner = "world" @ t[0]
+    s = f"hello {f'dear {inner @ t[1]}' @ t[2]}" @ t[3]
+
+
+@test
+def test_format_spec(t):
+    x = 3.14159 @ t[0]
+    s = f"{x @ t[1]:.2f}" @ t[2]
+
+
+@test
+def test_method_in_fstring(t):
+    name = "world" @ t[0]
+    s = f"hello {((name @ t[1]).upper @ t[2])() @ t[3]}" @ t[4]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_functions.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_functions.py
new file mode 100644
index 000000000000..e19b944c4cef
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_functions.py
@@ -0,0 +1,85 @@
+"""Function calls and definitions — evaluation order."""
+
+from timer import test
+
+
+@test
+def test_argument_order(t):
+    """Arguments evaluate left-to-right before the call."""
+    def add(a, b):
+        return (a @ t[3] + b @ t[4]) @ t[5]
+    result = (add @ t[0])(1 @ t[1], 2 @ t[2]) @ t[6]
+
+
+@test
+def test_multiple_arguments(t):
+    """All arguments left-to-right, then the call."""
+    def f(a, b, c):
+        return ((a @ t[4] + b @ t[5]) @ t[6] + c @ t[7]) @ t[8]
+    result = (f @ t[0])(1 @ t[1], 2 @ t[2], 3 @ t[3]) @ t[9]
+
+
+@test
+def test_default_arguments(t):
+    """Default expressions are evaluated at definition time."""
+    val = 5 @ t[0]
+    def f(a, b=val @ t[1]):
+        return (a @ t[4] + b @ t[5]) @ t[6]
+    result = (f @ t[2])(10 @ t[3]) @ t[7]
+
+
+@test
+def test_args_kwargs(t):
+    """*args and **kwargs — expressions evaluated before the call."""
+    def f(*args, **kwargs):
+        return ((sum @ t[9])(args @ t[10]) @ t[11] + (sum @ t[12])(((kwargs @ t[13]).values @ t[14])() @ t[15]) @ t[16]) @ t[17]
+    args = [1 @ t[0], 2 @ t[1]] @ t[2]
+    kwargs = {"c" @ t[3]: 3 @ t[4]} @ t[5]
+    result = (f @ t[6])(*args @ t[7], **kwargs @ t[8]) @ t[18]
+
+
+@test
+def test_nested_calls(t):
+    """Inner call completes before becoming an argument to outer call."""
+    def f(x):
+        return (x @ t[7] + 1 @ t[8]) @ t[9]
+    def g(x):
+        return (x @ t[3] * 2 @ t[4]) @ t[5]
+    result = (f @ t[0])((g @ t[1])(1 @ t[2]) @ t[6]) @ t[10]
+
+
+@test
+def test_function_as_argument(t):
+    """Function object is just another argument, evaluated left-to-right."""
+    def apply(fn, x):
+        return (fn @ t[3])(x @ t[4]) @ t[8]
+    def double(x):
+        return (x @ t[5] * 2 @ t[6]) @ t[7]
+    result = (apply @ t[0])(double @ t[1], 5 @ t[2]) @ t[9]
+
+
+@test
+def test_decorator(t):
+    """Decorator: expression evaluated, function defined, decorator called."""
+    def my_decorator(fn):
+        return fn @ t[1]
+    @(my_decorator @ t[0])
+    def f():
+        return 42 @ t[3]
+    result = (f @ t[2])() @ t[4]
+
+
+@test
+def test_keyword_arguments(t):
+    """Keyword argument values evaluate left-to-right."""
+    def f(a, b):
+        return (a @ t[3] + b @ t[4]) @ t[5]
+    result = (f @ t[0])(a=1 @ t[1], b=2 @ t[2]) @ t[6]
+
+
+@test
+def test_return_value(t):
+    """The return value is just the result of the call expression."""
+    def f(x):
+        return (x @ t[2] * 2 @ t[3]) @ t[4]
+    result = (f @ t[0])(3 @ t[1]) @ t[5]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py
new file mode 100644
index 000000000000..79abb278684c
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py
@@ -0,0 +1,114 @@
+"""If/elif/else control flow evaluation order."""
+
+from timer import test, dead
+
+
+@test
+def test_if_true(t):
+    x = True @ t[0]
+    if x @ t[1]:
+        y = 1 @ t[2]
+    z = 0 @ t[3]
+
+
+@test
+def test_if_false(t):
+    x = False @ t[0]
+    if x @ t[1]:
+        y = 1 @ t[dead(2)]
+    z = 0 @ t[2]
+
+
+@test
+def test_if_else_true(t):
+    x = True @ t[0]
+    if x @ t[1]:
+        y = 1 @ t[2]
+    else:
+        y = 2 @ t[dead(2)]
+    z = 0 @ t[3]
+
+
+@test
+def test_if_else_false(t):
+    x = False @ t[0]
+    if x @ t[1]:
+        y = 1 @ t[dead(2)]
+    else:
+        y = 2 @ t[2]
+    z = 0 @ t[3]
+
+
+@test
+def test_if_elif_else_first(t):
+    x = 1 @ t[0]
+    if (x @ t[1] == 1 @ t[2]) @ t[3]:
+        y = "first" @ t[4]
+    elif (x @ t[dead(4)] == 2 @ t[dead(5)]) @ t[dead(6)]:
+        y = "second" @ t[dead(4)]
+    else:
+        y = "third" @ t[dead(4)]
+    z = 0 @ t[5]
+
+
+@test
+def test_if_elif_else_second(t):
+    x = 2 @ t[0]
+    if (x @ t[1] == 1 @ t[2]) @ t[3]:
+        y = "first" @ t[dead(7)]
+    elif (x @ t[4] == 2 @ t[5]) @ t[6]:
+        y = "second" @ t[7]
+    else:
+        y = "third" @ t[dead(7)]
+    z = 0 @ t[8]
+
+
+@test
+def test_if_elif_else_third(t):
+    x = 3 @ t[0]
+    if (x @ t[1] == 1 @ t[2]) @ t[3]:
+        y = "first" @ t[dead(7)]
+    elif (x @ t[4] == 2 @ t[5]) @ t[6]:
+        y = "second" @ t[dead(7)]
+    else:
+        y = "third" @ t[7]
+    z = 0 @ t[8]
+
+
+@test
+def test_nested_if_else(t):
+    x = True @ t[0]
+    y = True @ t[1]
+    if x @ t[2]:
+        if y @ t[3]:
+            z = 1 @ t[4]
+        else:
+            z = 2 @ t[dead(4)]
+    else:
+        z = 3 @ t[dead(4)]
+    w = 0 @ t[5]
+
+
+@test
+def test_if_compound_condition(t):
+    x = True @ t[0]
+    y = False @ t[1]
+    if (x @ t[2] and y @ t[3]) @ t[4]:
+        z = 1 @ t[dead(5)]
+    else:
+        z = 2 @ t[5]
+    w = 0 @ t[6]
+
+
+@test
+def test_if_pass(t):
+    x = True @ t[0]
+    if x @ t[1]:
+        pass
+    z = 0 @ t[2]
+
+
+@test
+
+
+@test
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_lambda.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_lambda.py
new file mode 100644
index 000000000000..c60cbb5b3172
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_lambda.py
@@ -0,0 +1,46 @@
+"""Lambda expressions — evaluation order."""
+
+from timer import test
+
+
+@test
+def test_simple_lambda(t):
+    """Lambda creates a function object in one step."""
+    f = (lambda x: (x @ t[3] + 1 @ t[4]) @ t[5]) @ t[0]
+    result = (f @ t[1])(10 @ t[2]) @ t[6]
+
+
+@test
+def test_lambda_multiple_args(t):
+    """Lambda call: arguments evaluate left to right."""
+    f = (lambda a, b, c: ((a @ t[5] + b @ t[6]) @ t[7] + c @ t[8]) @ t[9]) @ t[0]
+    result = (f @ t[1])(1 @ t[2], 2 @ t[3], 3 @ t[4]) @ t[10]
+
+
+@test
+def test_lambda_default(t):
+    """Default argument evaluated at lambda creation time."""
+    val = 5 @ t[0]
+    f = (lambda x, y=val @ t[1]: (x @ t[5] + y @ t[6]) @ t[7]) @ t[2]
+    result = (f @ t[3])(10 @ t[4]) @ t[8]
+
+
+@test
+def test_lambda_map(t):
+    """Lambda body runs once per element when consumed by list(map(...))."""
+    f = (lambda x: (x @ t[9, 12, 15] * 2 @ t[10, 13, 16]) @ t[11, 14, 17]) @ t[0]
+    result = (list @ t[1])((map @ t[2])(f @ t[3], [1 @ t[4], 2 @ t[5], 3 @ t[6]] @ t[7]) @ t[8]) @ t[18]
+
+
+@test
+def test_immediately_invoked(t):
+    """Arguments evaluated, then immediately-invoked lambda called."""
+    result = ((lambda x: (x @ t[2] + 1 @ t[3]) @ t[4]) @ t[0])(10 @ t[1]) @ t[5]
+
+
+@test
+def test_lambda_closure(t):
+    """Lambda captures enclosing scope; body runs at call time."""
+    x = 10 @ t[0]
+    f = (lambda: x @ t[3]) @ t[1]
+    result = (f @ t[2])() @ t[4]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py
new file mode 100644
index 000000000000..17df7a4703a3
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_loops.py
@@ -0,0 +1,146 @@
+"""Loop control flow evaluation order tests."""
+
+from timer import test, dead
+
+
+# 1. Simple while loop (fixed iterations)
+@test
+def test_while_loop(t):
+    i = 0 @ t[0]
+    while (i @ t[1, 7, 13, 19] < 3 @ t[2, 8, 14, 20]) @ t[3, 9, 15, 21]:  # 4 checks: 3 true + 1 false
+        i = (i @ t[4, 10, 16] + 1 @ t[5, 11, 17]) @ t[6, 12, 18]
+    done = True @ t[22]
+
+
+# 2. While loop with break
+@test
+def test_while_break(t):
+    i = 0 @ t[0]
+    while (i @ t[1, 10, 19] < 5 @ t[2, 11, 20]) @ t[3, 12, 21]:
+        if (i @ t[4, 13, 22] == 2 @ t[5, 14, 23]) @ t[6, 15, 24]:
+            break
+        i = (i @ t[7, 16] + 1 @ t[8, 17]) @ t[9, 18]
+    done = True @ t[25]
+
+
+# 3. While loop with continue
+@test
+def test_while_continue(t):
+    i = 0 @ t[0]
+    total = 0 @ t[1]
+    while (i @ t[2, 14, 23, 35] < 3 @ t[3, 15, 24, 36]) @ t[4, 16, 25, 37]:
+        i = (i @ t[5, 17, 26] + 1 @ t[6, 18, 27]) @ t[7, 19, 28]
+        if (i @ t[8, 20, 29] == 2 @ t[9, 21, 30]) @ t[10, 22, 31]:
+            continue
+        total = (total @ t[11, 32] + i @ t[12, 33]) @ t[13, 34]
+    done = True @ t[38]
+
+
+# 4. While/else (no break — else executes)
+@test
+def test_while_else(t):
+    i = 0 @ t[0]
+    while (i @ t[1, 7, 13] < 2 @ t[2, 8, 14]) @ t[3, 9, 15]:
+        i = (i @ t[4, 10] + 1 @ t[5, 11]) @ t[6, 12]
+    else:
+        done = True @ t[16]
+
+
+# 5. While/else (with break — else skipped)
+@test
+def test_while_else_break(t):
+    i = 0 @ t[0]
+    while (i @ t[1, 10] < 5 @ t[2, 11]) @ t[3, 12]:
+        if (i @ t[4, 13] == 1 @ t[5, 14]) @ t[6, 15]:
+            break
+        i = (i @ t[7] + 1 @ t[8]) @ t[9]
+    else:
+        never = True @ t[dead(16)]
+    after = True @ t[16]
+
+
+# 6. Simple for loop over a list
+@test
+def test_for_list(t):
+    for x in [1 @ t[0], 2 @ t[1], 3 @ t[2]] @ t[3]:
+        x @ t[4, 5, 6]
+    done = True @ t[7]
+
+
+# 7. For loop with range
+@test
+def test_for_range(t):
+    for i in (range @ t[0])(3 @ t[1]) @ t[2]:
+        i @ t[3, 4, 5]
+    done = True @ t[6]
+
+
+# 8. For loop with break
+@test
+def test_for_break(t):
+    for x in [1 @ t[0], 2 @ t[1], 3 @ t[2], 4 @ t[3]] @ t[4]:
+        if (x @ t[5, 9, 13] == 3 @ t[6, 10, 14]) @ t[7, 11, 15]:
+            break
+        x @ t[8, 12]
+    done = True @ t[16]
+
+
+# 9. For loop with continue
+@test
+def test_for_continue(t):
+    total = 0 @ t[0]
+    for x in [1 @ t[1], 2 @ t[2], 3 @ t[3]] @ t[4]:
+        if (x @ t[5, 11, 14] == 2 @ t[6, 12, 15]) @ t[7, 13, 16]:
+            continue
+        total = (total @ t[8, 17] + x @ t[9, 18]) @ t[10, 19]
+    done = True @ t[20]
+
+
+# 10. For/else (no break — else executes)
+@test
+def test_for_else(t):
+    for x in [1 @ t[0], 2 @ t[1]] @ t[2]:
+        x @ t[3, 4]
+    else:
+        done = True @ t[5]
+
+
+# 11. For/else (with break — else skipped)
+@test
+def test_for_else_break(t):
+    for x in [1 @ t[0], 2 @ t[1], 3 @ t[2]] @ t[3]:
+        if (x @ t[4, 8] == 2 @ t[5, 9]) @ t[6, 10]:
+            break
+        x @ t[7]
+    else:
+        never = True @ t[dead(11)]
+    after = True @ t[11]
+
+
+# 12. Nested loops
+@test
+def test_nested_loops(t):
+    for i in [1 @ t[0], 2 @ t[1]] @ t[2]:
+        for j in [10 @ t[3, 12], 20 @ t[4, 13]] @ t[5, 14]:
+            (i @ t[6, 9, 15, 18, dead(21)] + j @ t[7, 10, 16, 19]) @ t[8, 11, 17, 20]
+    done = True @ t[dead(3), dead(6), dead(9), dead(12), dead(15), dead(18), 21]
+
+
+# 13. While True with conditional break
+@test
+def test_while_true_break(t):
+    i = 0 @ t[0]
+    while True @ t[1, 8, 15]:
+        i = (i @ t[2, 9, 16] + 1 @ t[3, 10, 17]) @ t[4, 11, 18]
+        if (i @ t[5, 12, 19] == 3 @ t[6, 13, 20]) @ t[7, 14, 21]:
+            break
+    done = True @ t[22]
+
+
+# 14. For with enumerate
+@test
+def test_for_enumerate(t):
+    for idx, val in (enumerate @ t[0])(["a" @ t[1], "b" @ t[2], "c" @ t[3]] @ t[4]) @ t[5]:
+        idx @ t[6, 8, 10]
+        val @ t[7, 9, 11]
+    done = True @ t[12]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py
new file mode 100644
index 000000000000..ba15a2d7c857
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_match.py
@@ -0,0 +1,173 @@
+"""Evaluation order for match/case (structural pattern matching, Python 3.10+)."""
+
+import sys
+if sys.version_info < (3, 10):
+    print("Skipping match/case tests (requires Python 3.10+)")
+    print("---")
+    print("0/0 tests passed")
+    sys.exit(0)
+
+from timer import test, dead, never
+
+
+@test
+def test_match_literal(t):
+    x = 1 @ t[0]
+    match x @ t[1]:
+        case 1:
+            y = "one" @ t[2]
+        case 2:
+            y = "two" @ t[dead(2)]
+    z = y @ t[3]
+
+
+@test
+def test_match_literal_fallthrough(t):
+    x = 3 @ t[0]
+    match x @ t[1]:
+        case 1:
+            y = "one" @ t[dead(2)]
+        case 2:
+            y = "two" @ t[dead(2)]
+        case 3:
+            y = "three" @ t[2]
+    z = y @ t[3]
+
+
+@test
+def test_match_wildcard(t):
+    x = 42 @ t[0]
+    match x @ t[1]:
+        case 1:
+            y = "one" @ t[dead(2)]
+        case _:
+            y = "other" @ t[2]
+    z = y @ t[3]
+
+
+@test
+def test_match_capture(t):
+    x = 42 @ t[0]
+    match x @ t[1]:
+        case n:
+            y = n @ t[2]
+    z = y @ t[3]
+
+
+@test
+def test_match_or_pattern(t):
+    x = 2 @ t[0]
+    match x @ t[1]:
+        case 1 | 2:
+            y = "low" @ t[2]
+        case _:
+            y = "other" @ t[dead(2)]
+    z = y @ t[3]
+
+
+@test
+def test_match_guard(t):
+    x = 5 @ t[0]
+    match x @ t[1]:
+        case n if (n @ t[2] > 3 @ t[3]) @ t[4]:
+            y = n @ t[5]
+        case _:
+            y = 0 @ t[dead(5)]
+    z = y @ t[6]
+
+
+@test
+def test_match_class_pattern(t):
+    x = 42 @ t[0]
+    match x @ t[1]:
+        case int():
+            y = "integer" @ t[2]
+        case str():
+            y = "string" @ t[dead(2)]
+    z = y @ t[3]
+
+
+@test
+def test_match_sequence(t):
+    x = [1 @ t[0], 2 @ t[1]] @ t[2]
+    match x @ t[3]:
+        case [a, b]:
+            y = (a @ t[4] + b @ t[5]) @ t[6]
+        case _:
+            y = 0 @ t[dead(6)]
+    z = y @ t[7]
+
+
+@test
+def test_match_mapping(t):
+    x = {"key" @ t[0]: 42 @ t[1]} @ t[2]
+    match x @ t[3]:
+        case {"key": value}:
+            y = value @ t[4]
+        case _:
+            y = 0 @ t[dead(4)]
+    z = y @ t[5]
+
+
+@test
+def test_match_nested(t):
+    x = {"users" @ t[0]: [{"name" @ t[1]: "Alice" @ t[2]} @ t[3]] @ t[4]} @ t[5]
+    match x @ t[6]:
+        case {"users": [{"name": name}]}:
+            y = name @ t[7]
+        case _:
+            y = "unknown" @ t[dead(7)]
+    z = y @ t[8]
+
+
+@test
+def test_match_or_pattern_with_as(t):
+    """OR pattern with `as` binding and method call on the result."""
+    clause = "foo@bar" @ t[0]
+    match clause @ t[1]:
+        case (str() as uses) | {"uses": uses}:
+            result = ((uses @ t[2]).partition @ t[3])("@" @ t[4]) @ t[5]
+            x = (result @ t[6])[0 @ t[7]] @ t[8]
+        case _:
+            raise ((ValueError @ t[dead(2)])(clause @ t[dead(3)]) @ t[dead(4)])
+    y = x @ t[9]
+
+
+@test
+def test_match_wildcard_raise(t):
+    """Wildcard case that raises, with OR pattern on the other branch."""
+    clause = 42 @ t[0]
+    try:
+        match clause @ t[1]:
+            case (str() as uses) | {"uses": uses}:
+                result = uses @ t[dead(2)]
+            case _:
+                raise ((ValueError @ t[2])(f"Invalid: {clause @ t[3]}" @ t[4]) @ t[5])
+    except ValueError:
+        y = 0 @ t[6]
+
+
+@test
+def test_match_exhaustive_return_first(t):
+    """Every case returns; code after match is unreachable (first case taken)."""
+    def f(x):
+        match x @ t[2]:
+            case 1:
+                return "one" @ t[3]
+            case _:
+                return "other" @ t[dead(3)]
+        y = 0 @ t[never]
+    result = (f @ t[0])(1 @ t[1]) @ t[4]
+
+
+@test
+def test_match_exhaustive_return_wildcard(t):
+    """Every case returns; code after match is unreachable (wildcard taken)."""
+    def f(x):
+        match x @ t[2]:
+            case 1:
+                return "one" @ t[dead(3)]
+            case _:
+                return "other" @ t[3]
+        y = 0 @ t[never]
+    result = (f @ t[0])(99 @ t[1]) @ t[4]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py
new file mode 100644
index 000000000000..dd0b15457d69
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_try.py
@@ -0,0 +1,182 @@
+"""Exception handling control flow: try/except/else/finally evaluation order."""
+
+from timer import test, dead, never
+
+
+# 1. try/except — no exception raised (except block skipped)
+@test
+def test_try_no_exception(t):
+    try:
+        x = 1 @ t[0]
+        y = 2 @ t[1]
+    except ValueError:
+        z = 3 @ t[dead(2)]
+    after = 0 @ t[2]
+
+
+# 2. try/except — exception raised and caught
+@test
+def test_try_with_exception(t):
+    try:
+        x = 1 @ t[0]
+        raise ((ValueError @ t[1])() @ t[2])
+        y = 2 @ t[never]
+    except ValueError:
+        z = 3 @ t[3]
+    after = 0 @ t[4]
+
+
+# 3. try/except/else — no exception (else runs)
+@test
+def test_try_except_else_no_exception(t):
+    try:
+        x = 1 @ t[0]
+    except ValueError:
+        y = 2 @ t[dead(1)]
+    else:
+        z = 3 @ t[1]
+    after = 0 @ t[2]
+
+
+# 4. try/except/else — exception raised (else skipped)
+@test
+def test_try_except_else_with_exception(t):
+    try:
+        x = 1 @ t[0]
+        raise ((ValueError @ t[1])() @ t[2])
+    except ValueError:
+        y = 2 @ t[3]
+    else:
+        z = 3 @ t[dead(3)]
+    after = 0 @ t[4]
+
+
+# 5. try/finally — no exception
+@test
+def test_try_finally_no_exception(t):
+    try:
+        x = 1 @ t[0]
+        y = 2 @ t[1]
+    finally:
+        z = 3 @ t[2]
+    after = 0 @ t[3]
+
+
+# 6. try/finally — exception raised (finally runs, then exception propagates)
+@test
+def test_try_finally_exception(t):
+    try:
+        try:
+            x = 1 @ t[0]
+            raise ((ValueError @ t[1])() @ t[2])
+        finally:
+            y = 2 @ t[3]
+    except ValueError:
+        z = 3 @ t[4]
+
+
+# 7. try/except/finally — no exception
+@test
+def test_try_except_finally_no_exception(t):
+    try:
+        x = 1 @ t[0]
+    except ValueError:
+        y = 2 @ t[dead(1)]
+    finally:
+        z = 3 @ t[1]
+    after = 0 @ t[2]
+
+
+# 8. try/except/finally — exception caught
+@test
+def test_try_except_finally_exception(t):
+    try:
+        x = 1 @ t[0]
+        raise ((ValueError @ t[1])() @ t[2])
+    except ValueError:
+        y = 2 @ t[3]
+    finally:
+        z = 3 @ t[4]
+    after = 0 @ t[5]
+
+
+# 9. Multiple except clauses — first matching
+@test
+def test_multiple_except_first(t):
+    try:
+        x = 1 @ t[0]
+        raise ((ValueError @ t[1])() @ t[2])
+    except ValueError:
+        y = 2 @ t[3]
+    except TypeError:
+        z = 3 @ t[dead(3)]
+    after = 0 @ t[4]
+
+
+# 10. Multiple except clauses — second matching
+@test
+def test_multiple_except_second(t):
+    try:
+        x = 1 @ t[0]
+        raise ((TypeError @ t[1])() @ t[2])
+    except ValueError:
+        y = 2 @ t[dead(3)]
+    except TypeError:
+        z = 3 @ t[3]
+    after = 0 @ t[4]
+
+
+# 11. except with `as` binding
+@test
+def test_except_as_binding(t):
+    try:
+        x = 1 @ t[0]
+        raise ((ValueError @ t[1])("msg" @ t[2]) @ t[3])
+    except ValueError as e:
+        y = (str @ t[4])(e @ t[5]) @ t[6]
+    after = 0 @ t[7]
+
+
+# 12. Nested try/except
+@test
+def test_nested_try_except(t):
+    try:
+        x = 1 @ t[0]
+        try:
+            y = 2 @ t[1]
+            raise ((ValueError @ t[2])() @ t[3])
+        except ValueError:
+            z = 3 @ t[4]
+        w = 4 @ t[5]
+    except TypeError:
+        v = 5 @ t[dead(6)]
+    after = 0 @ t[6]
+
+
+# 13. try/except in a loop
+@test
+def test_try_in_loop(t):
+    total = 0 @ t[0]
+    for i in (range @ t[1])(3 @ t[2]) @ t[3]:
+        try:
+            if (i @ t[4, 11, 20] == 1 @ t[5, 12, 21]) @ t[6, 13, 22]:
+                raise ((ValueError @ t[14])() @ t[15])
+            total = (total @ t[7, 23] + 1 @ t[8, 24]) @ t[9, 25]
+        except ValueError:
+            total = (total @ t[16] + 10 @ t[17]) @ t[18]
+        r = 0 @ t[10, 19, 26]
+
+
+# 14. Re-raise with bare `raise`
+@test
+def test_reraise(t):
+    try:
+        try:
+            x = 1 @ t[0]
+            raise ((ValueError @ t[1])() @ t[2])
+        except ValueError:
+            y = 2 @ t[3]
+            raise
+    except ValueError:
+        z = 3 @ t[4]
+    after = 0 @ t[5]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_unpacking.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_unpacking.py
new file mode 100644
index 000000000000..45f292cb0b7d
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_unpacking.py
@@ -0,0 +1,48 @@
+"""Unpacking and star expressions evaluation order."""
+
+from timer import test
+
+
+@test
+def test_tuple_unpack(t):
+    """RHS expression evaluates, then unpacking assigns targets."""
+    a, b = (1 @ t[0], 2 @ t[1]) @ t[2]
+    x = (a @ t[3] + b @ t[4]) @ t[5]
+
+
+@test
+def test_list_unpack(t):
+    """List unpacking: RHS elements left to right, then unpack."""
+    [a, b] = [1 @ t[0], 2 @ t[1]] @ t[2]
+    x = (a @ t[3] + b @ t[4]) @ t[5]
+
+
+@test
+def test_star_unpack(t):
+    """Star unpacking: RHS evaluates first."""
+    a, *b = [1 @ t[0], 2 @ t[1], 3 @ t[2], 4 @ t[3]] @ t[4]
+    x = (a @ t[5], b @ t[6]) @ t[7]
+
+
+@test
+def test_nested_unpack(t):
+    """Nested unpacking: RHS evaluates first."""
+    (a, b), c = ((1 @ t[0], 2 @ t[1]) @ t[2], 3 @ t[3]) @ t[4]
+    x = ((a @ t[5] + b @ t[6]) @ t[7] + c @ t[8]) @ t[9]
+
+
+@test
+def test_swap(t):
+    a = 1 @ t[0]
+    b = 2 @ t[1]
+    a, b = (b @ t[2], a @ t[3]) @ t[4]
+    x = a @ t[5]
+    y = b @ t[6]
+
+
+@test
+def test_unpack_for(t):
+    pairs = [(1 @ t[0], 2 @ t[1]) @ t[2], (3 @ t[3], 4 @ t[4]) @ t[5]] @ t[6]
+    for a, b in pairs @ t[7]:
+        x = a @ t[8, 10]
+        y = b @ t[9, 11]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_with.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_with.py
new file mode 100644
index 000000000000..1dcc7169092b
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_with.py
@@ -0,0 +1,58 @@
+"""Evaluation order tests for with statements."""
+
+from contextlib import contextmanager
+from timer import test
+
+
+@contextmanager
+def ctx(value=None):
+    yield value
+
+
+@test
+def test_simple_with(t):
+    x = 1 @ t[0]
+    with (ctx @ t[1])() @ t[2]:
+        y = 2 @ t[3]
+    z = 3 @ t[4]
+
+
+@test
+def test_with_as(t):
+    with (ctx @ t[0])(42 @ t[1]) @ t[2] as v:
+        x = v @ t[3]
+    y = 0 @ t[4]
+
+
+@test
+def test_nested_with(t):
+    with (ctx @ t[0])() @ t[1]:
+        with (ctx @ t[2])() @ t[3]:
+            x = 1 @ t[4]
+    y = 2 @ t[5]
+
+
+@test
+def test_multiple_context_managers(t):
+    with (ctx @ t[0])(1 @ t[1]) @ t[2] as a, (ctx @ t[3])(2 @ t[4]) @ t[5] as b:
+        x = (a @ t[6], b @ t[7]) @ t[8]
+    y = 0 @ t[9]
+
+
+@test
+def test_with_exception_handling(t):
+    try:
+        with (ctx @ t[0])() @ t[1]:
+            x = 1 @ t[2]
+            raise ((ValueError @ t[3])() @ t[4])
+    except ValueError:
+        y = 2 @ t[5]
+    z = 3 @ t[6]
+
+
+@test
+def test_with_in_loop(t):
+    for i in [1 @ t[0], 2 @ t[1]] @ t[2]:
+        with (ctx @ t[3, 6])() @ t[4, 7]:
+            x = i @ t[5, 8]
+    y = 0 @ t[9]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/test_yield.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_yield.py
new file mode 100644
index 000000000000..b2a28d793bc6
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_yield.py
@@ -0,0 +1,105 @@
+"""Generator and yield evaluation order tests.
+
+Generator bodies are lazy — code runs only when iterated.  The timer
+annotations inside generator bodies fire interleaved with the caller's
+annotations, reflecting the suspend/resume semantics of yield.
+"""
+
+from timer import test
+
+
+@test
+def test_simple_generator(t):
+    """Basic generator: body runs on next(), not on gen()."""
+    def gen():
+        yield 1 @ t[4]
+        yield 2 @ t[8]
+
+    g = (gen @ t[0])() @ t[1]
+    x = (next @ t[2])(g @ t[3]) @ t[5]
+    y = (next @ t[6])(g @ t[7]) @ t[9]
+
+
+@test
+def test_multiple_yields(t):
+    """Three yields interleave with three next() calls."""
+    def gen():
+        yield 1 @ t[4]
+        yield 2 @ t[8]
+        yield 3 @ t[12]
+
+    g = (gen @ t[0])() @ t[1]
+    a = (next @ t[2])(g @ t[3]) @ t[5]
+    b = (next @ t[6])(g @ t[7]) @ t[9]
+    c = (next @ t[10])(g @ t[11]) @ t[13]
+
+
+@test
+def test_generator_for_loop(t):
+    """for-loop consumes generator, interleaving body and loop."""
+    def gen():
+        yield 1 @ t[2]
+        yield 2 @ t[4]
+
+    for val in (gen @ t[0])() @ t[1]:
+        val @ t[3, 5]
+
+
+@test
+def test_generator_list(t):
+    """list() consumes the entire generator without interleaving."""
+    def gen():
+        yield 10 @ t[3]
+        yield 20 @ t[4]
+        yield 30 @ t[5]
+
+    result = (list @ t[0])((gen @ t[1])() @ t[2]) @ t[6]
+
+
+@test
+def test_yield_from(t):
+    """yield from delegates to an inner generator transparently."""
+    def inner():
+        yield 1 @ t[6]
+        yield 2 @ t[10]
+
+    def outer():
+        yield from (inner @ t[4])() @ t[5]
+
+    g = (outer @ t[0])() @ t[1]
+    x = (next @ t[2])(g @ t[3]) @ t[7]
+    y = (next @ t[8])(g @ t[9]) @ t[11]
+
+
+@test
+def test_generator_return(t):
+    """Generator return value accessed via yield from."""
+    def gen():
+        yield 1 @ t[6]
+        return 42 @ t[10]
+
+    def wrapper():
+        result = (yield from (gen @ t[4])() @ t[5]) @ t[11]
+        yield result @ t[12]
+
+    g = (wrapper @ t[0])() @ t[1]
+    x = (next @ t[2])(g @ t[3]) @ t[7]
+    y = (next @ t[8])(g @ t[9]) @ t[13]
+
+
+@test
+def test_generator_send(t):
+    """send() passes a value into the generator at the yield point."""
+    def gen():
+        x = (yield 1 @ t[4]) @ t[9]
+        yield (x @ t[10] + 10 @ t[11]) @ t[12]
+
+    g = (gen @ t[0])() @ t[1]
+    first = (next @ t[2])(g @ t[3]) @ t[5]
+    second = ((g @ t[6]).send @ t[7])(42 @ t[8]) @ t[13]
+
+
+@test
+def test_generator_expression(t):
+    """Inline generator expression consumed by list()."""
+    result = (list @ t[0])(x @ t[5, 6, 7] for x in [10 @ t[1], 20 @ t[2], 30 @ t[3]] @ t[4]) @ t[8]
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py b/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py
new file mode 100644
index 000000000000..e10dde2592af
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py
@@ -0,0 +1,189 @@
+"""Abstract timer for self-validating CFG evaluation-order tests.
+
+Provides a Timer context manager and a @test decorator for writing tests
+that verify the order in which Python evaluates expressions.
+
+Usage with @test decorator (preferred):
+
+    from timer import test, dead, never
+
+    @test
+    def test_sequential(t):
+        x = 1 @ t[0]
+        y = 2 @ t[1]
+        z = (x + y) @ t[2]
+
+Annotation forms:
+    t[n]              - assert current timestamp is n, return marker
+    t[n, m, ...]      - assert current timestamp is one of {n, m, ...}
+    t[dead(n)]        - mark timestamp n as dead (fails if evaluated)
+    t[dead(n), m]     - dead at n, live at m
+    t[never]          - mark as never evaluated (fails if evaluated)
+    t["label"]        - record current timestamp under label (development aid)
+    t(value, n)       - equivalent to: value @ t[n]
+
+Run a test file directly to self-validate: python test_file.py
+"""
+
+import atexit
+import sys
+
+_results = []
+
+
+class _Check:
+    """Marker returned by t[n] — asserts the current timestamp.
+
+    Receives the raw subscript elements: plain ints are live timestamps,
+    dead(n) markers are dead timestamps, and `never` means any evaluation
+    is an error.
+    """
+
+    __slots__ = ("_timer", "_live", "_dead", "_never")
+
+    def __init__(self, timer, elements):
+        self._timer = timer
+        self._live = set()
+        self._dead = set()
+        self._never = False
+        for e in elements:
+            if isinstance(e, int):
+                self._live.add(e)
+            elif isinstance(e, _DeadMarker):
+                self._dead.add(e.timestamp)
+            elif isinstance(e, _NeverSentinel):
+                self._never = True
+
+    def __rmatmul__(self, value):
+        ts = self._timer._tick()
+        if self._never:
+            self._timer._error(
+                f"expression annotated with t[never] was evaluated (timestamp {ts})"
+            )
+        elif ts in self._dead:
+            self._timer._error(
+                f"timestamp {ts} is marked dead but was evaluated"
+            )
+        elif ts not in self._live:
+            self._timer._error(
+                f"expected {sorted(self._live)}, got {ts}"
+            )
+        return value
+
+
+class _Label:
+    """Marker returned by t["name"] — records the timestamp under a label."""
+
+    __slots__ = ("_timer", "_name")
+
+    def __init__(self, timer, name):
+        self._timer = timer
+        self._name = name
+
+    def __rmatmul__(self, value):
+        ts = self._timer._tick()
+        self._timer._labels.setdefault(self._name, []).append(ts)
+        return value
+
+
+class _DeadMarker:
+    """Marker returned by dead(n) — used inside t[...] to mark a timestamp as dead."""
+
+    def __init__(self, timestamp):
+        self.timestamp = timestamp
+
+
+def dead(n):
+    """Mark timestamp `n` as dead code inside a timer subscript: t[dead(1), 2]."""
+    return _DeadMarker(n)
+
+
+class _NeverSentinel:
+    """Sentinel for never-evaluated annotations: t[never]."""
+    pass
+
+
+never = _NeverSentinel()
+
+
+class Timer:
+    """Context manager tracking abstract evaluation timestamps.
+
+    Each Timer instance maintains a counter starting at 0. Every time an
+    annotation (@ t[n] or t(value, n)) is encountered, the counter is
+    compared against the expected value and then incremented.
+    """
+
+    def __init__(self, name="<unnamed>"):
+        self._name = name
+        self._counter = 0
+        self._errors = []
+        self._labels = {}
+
+    def __enter__(self):
+        return self
+
+    def __exit__(self, exc_type, exc_val, exc_tb):
+        if self._labels:
+            for name, timestamps in sorted(self._labels.items()):
+                print(f"  {name}: {', '.join(map(str, timestamps))}")
+        _results.append((self._name, list(self._errors)))
+        if self._errors:
+            print(f"{self._name}: FAIL")
+            for err in self._errors:
+                print(f"  {err}")
+        else:
+            print(f"{self._name}: ok")
+        return False
+
+    def _tick(self):
+        ts = self._counter
+        self._counter += 1
+        return ts
+
+    def _error(self, msg):
+        self._errors.append(msg)
+
+    def __getitem__(self, key):
+        if isinstance(key, str):
+            return _Label(self, key)
+        elif isinstance(key, tuple):
+            return _Check(self, key)
+        else:
+            return _Check(self, [key])
+
+    def __call__(self, value, key):
+        """Alternative to @ operator: t(value, 4) or t(value, [1, 2, 3])."""
+        if isinstance(key, list):
+            key = tuple(key)
+        marker = self[key]
+        return marker.__rmatmul__(value)
+
+
+def test(fn):
+    """Decorator that creates a Timer and runs the test function immediately.
+
+    The function receives a fresh Timer as its sole argument. Errors are
+    collected (not raised) and reported after the function completes.
+    """
+    with Timer(fn.__name__) as t:
+        try:
+            fn(t)
+        except Exception as e:
+            t._error(f"exception: {type(e).__name__}: {e}")
+    return fn
+
+
+def _report():
+    """Print summary at interpreter exit."""
+    if not _results:
+        return
+    total = len(_results)
+    passed = sum(1 for _, errors in _results if not errors)
+    print("---")
+    print(f"{passed}/{total} tests passed")
+    if passed < total:
+        sys.exit(1)
+
+
+atexit.register(_report)

From edfbaa5cebd137dc430b385f497f70a9e9e3a216 Mon Sep 17 00:00:00 2001
From: Taus <tausbn@github.com>
Date: Tue, 28 Apr 2026 15:06:50 +0000
Subject: [PATCH 2/5] Python: Add some CFG-validation queries

These use the annotated, self-verifying test files to check various
consistency requirements.

Some of these may be expressing the same thing in different ways, but
it's fairly cheap to keep them around, so I have not attempted to
produce a minimal set of queries for this.
---
 .../AllLiveReachable.expected                 |  0
 .../evaluation-order/AllLiveReachable.ql      | 18 +++++++++++++++
 .../AnnotationHasCfgNode.expected             |  1 +
 .../evaluation-order/AnnotationHasCfgNode.ql  | 15 +++++++++++++
 .../BasicBlockAnnotationGap.expected          |  0
 .../BasicBlockAnnotationGap.ql                | 22 +++++++++++++++++++
 .../ContiguousTimestamps.expected             |  0
 .../evaluation-order/ContiguousTimestamps.ql  | 17 ++++++++++++++
 .../evaluation-order/NoBackwardFlow.expected  | 10 +++++++++
 .../evaluation-order/NoBackwardFlow.ql        | 18 +++++++++++++++
 .../evaluation-order/NoBasicBlock.expected    |  1 +
 .../evaluation-order/NoBasicBlock.ql          | 15 +++++++++++++
 .../NoSharedReachable.expected                |  0
 .../evaluation-order/NoSharedReachable.ql     | 17 ++++++++++++++
 .../evaluation-order/StrictForward.expected   | 10 +++++++++
 .../evaluation-order/StrictForward.ql         | 18 +++++++++++++++
 16 files changed, 162 insertions(+)
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql

diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql
new file mode 100644
index 000000000000..314b6f4ca4da
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql
@@ -0,0 +1,18 @@
+/**
+ * Checks that every live (non-dead) annotation in the test function's
+ * own scope is reachable from the function entry in the CFG.
+ * Annotations in nested scopes (generators, async, lambdas, comprehensions)
+ * have separate CFGs and are excluded from this check.
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from TimerCfgNode a, TestFunction f
+where allLiveReachable(a, f)
+select a, "Unreachable live annotation; entry of $@ does not reach this node", f, f.getName()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.expected
new file mode 100644
index 000000000000..8b137891791f
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.expected
@@ -0,0 +1 @@
+
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.ql
new file mode 100644
index 000000000000..4dbe5cbdcea7
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.ql
@@ -0,0 +1,15 @@
+/**
+ * Checks that every timer annotation has a corresponding CFG node.
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils::CfgTests
+
+from TimerAnnotation ann
+where annotationWithoutCfgNode(ann)
+select ann, "Annotation in $@ has no CFG node", ann.getTestFunction(),
+  ann.getTestFunction().getName()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql
new file mode 100644
index 000000000000..4bb53f6fb612
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql
@@ -0,0 +1,22 @@
+/**
+ * Checks that within a basic block, if a node is annotated then its
+ * successor is also annotated (or excluded). A gap in annotations
+ * within a basic block indicates a missing annotation, since there
+ * are no branches to justify the gap.
+ *
+ * Nodes with exceptional successors are excluded, as the exception
+ * edge leaves the basic block and the normal successor may be dead.
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from TimerCfgNode a, CfgNode succ
+where basicBlockAnnotationGap(a, succ)
+select a, "Annotated node followed by unannotated $@ in the same basic block", succ,
+  succ.getNode().toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql
new file mode 100644
index 000000000000..f18c52750b52
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql
@@ -0,0 +1,17 @@
+/**
+ * Checks that timestamps form a contiguous sequence {0, 1, ..., max}
+ * within each test function. Every integer in the range must appear
+ * in at least one annotation (live or dead).
+ */
+
+import TimerUtils
+
+from TestFunction f, int missing, int maxTs, TimerAnnotation maxAnn
+where
+  maxTs = max(TimerAnnotation a | a.getTestFunction() = f | a.getATimestamp()) and
+  maxAnn.getTestFunction() = f and
+  maxAnn.getATimestamp() = maxTs and
+  missing = [0 .. maxTs] and
+  not exists(TimerAnnotation a | a.getTestFunction() = f and a.getATimestamp() = missing)
+select f, "Missing timestamp " + missing + " (max is $@)", maxAnn.getTimestampExpr(maxTs),
+  maxTs.toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.expected
new file mode 100644
index 000000000000..1ef8be08d27b
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.expected
@@ -0,0 +1,10 @@
+| test_boolean.py:9:10:9:43 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:9:59:9:59 | IntegerLiteral | 2 | test_boolean.py:9:10:9:13 | ControlFlowNode for True | True | test_boolean.py:9:19:9:19 | IntegerLiteral | 0 |
+| test_boolean.py:15:10:15:43 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:15:50:15:50 | IntegerLiteral | 1 | test_boolean.py:15:10:15:14 | ControlFlowNode for False | False | test_boolean.py:15:20:15:20 | IntegerLiteral | 0 |
+| test_boolean.py:21:10:21:42 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:21:49:21:49 | IntegerLiteral | 1 | test_boolean.py:21:10:21:13 | ControlFlowNode for True | True | test_boolean.py:21:19:21:19 | IntegerLiteral | 0 |
+| test_boolean.py:27:10:27:43 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:27:59:27:59 | IntegerLiteral | 2 | test_boolean.py:27:10:27:14 | ControlFlowNode for False | False | test_boolean.py:27:20:27:20 | IntegerLiteral | 0 |
+| test_boolean.py:40:10:40:61 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:40:86:40:86 | IntegerLiteral | 3 | test_boolean.py:40:10:40:10 | ControlFlowNode for IntegerLiteral | IntegerLiteral | test_boolean.py:40:16:40:16 | IntegerLiteral | 0 |
+| test_boolean.py:46:10:46:61 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:46:86:46:86 | IntegerLiteral | 3 | test_boolean.py:46:10:46:10 | ControlFlowNode for IntegerLiteral | IntegerLiteral | test_boolean.py:46:16:46:16 | IntegerLiteral | 0 |
+| test_boolean.py:52:10:52:95 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:52:120:52:120 | IntegerLiteral | 4 | test_boolean.py:52:11:52:47 | ControlFlowNode for BoolExpr | BoolExpr | test_boolean.py:52:63:52:63 | IntegerLiteral | 2 |
+| test_boolean.py:52:11:52:47 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:52:63:52:63 | IntegerLiteral | 2 | test_boolean.py:52:11:52:14 | ControlFlowNode for True | True | test_boolean.py:52:20:52:20 | IntegerLiteral | 0 |
+| test_boolean.py:64:10:64:52 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:64:59:64:59 | IntegerLiteral | 6 | test_boolean.py:64:11:64:11 | ControlFlowNode for f | f | test_boolean.py:64:17:64:17 | IntegerLiteral | 0 |
+| test_boolean.py:76:10:76:51 | ControlFlowNode for BoolExpr | Backward flow: $@ flows to $@ (max timestamp $@) | test_boolean.py:76:58:76:58 | IntegerLiteral | 6 | test_boolean.py:76:11:76:11 | ControlFlowNode for f | f | test_boolean.py:76:17:76:17 | IntegerLiteral | 0 |
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql
new file mode 100644
index 000000000000..a94e6b3319f7
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql
@@ -0,0 +1,18 @@
+/**
+ * Checks that time never flows backward between consecutive timer annotations
+ * in the CFG. For each pair of consecutive annotated nodes (A -> B), there must
+ * exist timestamps a in A and b in B with a < b.
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from TimerCfgNode a, TimerCfgNode b, int minA, int maxB
+where noBackwardFlow(a, b, minA, maxB)
+select a, "Backward flow: $@ flows to $@ (max timestamp $@)", a.getTimestampExpr(minA),
+  minA.toString(), b, b.getNode().toString(), b.getTimestampExpr(maxB), maxB.toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.expected
new file mode 100644
index 000000000000..8b137891791f
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.expected
@@ -0,0 +1 @@
+
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.ql
new file mode 100644
index 000000000000..21a1b2a29dd3
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.ql
@@ -0,0 +1,15 @@
+/**
+ * Checks that every annotated CFG node belongs to a basic block.
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from CfgNode n, TestFunction f
+where noBasicBlock(n, f)
+select n, "CFG node in $@ does not belong to any basic block", f, f.getName()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql
new file mode 100644
index 000000000000..744b107a6708
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql
@@ -0,0 +1,17 @@
+/**
+ * Checks that two annotations sharing a timestamp value are on
+ * mutually exclusive CFG paths (neither can reach the other).
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from TimerCfgNode a, TimerCfgNode b, int ts
+where noSharedReachable(a, b, ts)
+select a, "Shared timestamp $@ but this node reaches $@", a.getTimestampExpr(ts), ts.toString(), b,
+  b.getNode().toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.expected
new file mode 100644
index 000000000000..aa03001b61bd
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.expected
@@ -0,0 +1,10 @@
+| test_boolean.py:9:10:9:43 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:9:59:9:59 | IntegerLiteral | timestamp 2 | test_boolean.py:9:19:9:19 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:15:10:15:43 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:15:50:15:50 | IntegerLiteral | timestamp 1 | test_boolean.py:15:20:15:20 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:21:10:21:42 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:21:49:21:49 | IntegerLiteral | timestamp 1 | test_boolean.py:21:19:21:19 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:27:10:27:43 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:27:59:27:59 | IntegerLiteral | timestamp 2 | test_boolean.py:27:20:27:20 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:40:10:40:61 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:40:86:40:86 | IntegerLiteral | timestamp 3 | test_boolean.py:40:16:40:16 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:46:10:46:61 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:46:86:46:86 | IntegerLiteral | timestamp 3 | test_boolean.py:46:16:46:16 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:52:10:52:95 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:52:120:52:120 | IntegerLiteral | timestamp 4 | test_boolean.py:52:63:52:63 | IntegerLiteral | timestamp 2 |
+| test_boolean.py:52:11:52:47 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:52:63:52:63 | IntegerLiteral | timestamp 2 | test_boolean.py:52:20:52:20 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:64:10:64:52 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:64:59:64:59 | IntegerLiteral | timestamp 6 | test_boolean.py:64:17:64:17 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:76:10:76:51 | ControlFlowNode for BoolExpr | Strict forward violation: $@ flows to $@ | test_boolean.py:76:58:76:58 | IntegerLiteral | timestamp 6 | test_boolean.py:76:17:76:17 | IntegerLiteral | timestamp 0 |
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql
new file mode 100644
index 000000000000..ac7555318960
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql
@@ -0,0 +1,18 @@
+/**
+ * Stronger version of NoBackwardFlow: for consecutive annotated nodes
+ * A -> B that both have a single timestamp (non-loop code) and B does
+ * NOT dominate A (forward edge), requires max(A) < min(B).
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from TimerCfgNode a, TimerCfgNode b, int maxA, int minB
+where strictForward(a, b, maxA, minB)
+select a, "Strict forward violation: $@ flows to $@", a.getTimestampExpr(maxA), "timestamp " + maxA,
+  b.getTimestampExpr(minB), "timestamp " + minB

From e5943cd4f7d9272cecb99e75ea2ccae72f3de1b5 Mon Sep 17 00:00:00 2001
From: Taus <tausbn@github.com>
Date: Tue, 28 Apr 2026 15:06:56 +0000
Subject: [PATCH 3/5] Python: Add BasicBlockOrdering test

This one demonstrates a bug in the current CFG. In a dictionary
comprehension `{k: v for k, v in d.items()}`, we evaluate the value
before the key, which is incorrect. (A fix for this bug has been
implemented in a separate PR.)
---
 .../BasicBlockOrdering.expected                 | 13 +++++++++++++
 .../evaluation-order/BasicBlockOrdering.ql      | 17 +++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.ql

diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.expected
new file mode 100644
index 000000000000..80fa3350282f
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.expected
@@ -0,0 +1,13 @@
+| test_boolean.py:9:10:9:43 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:9:59:9:59 | IntegerLiteral | timestamp 2 | test_boolean.py:9:19:9:19 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:15:10:15:43 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:15:50:15:50 | IntegerLiteral | timestamp 1 | test_boolean.py:15:20:15:20 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:21:10:21:42 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:21:49:21:49 | IntegerLiteral | timestamp 1 | test_boolean.py:21:19:21:19 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:27:10:27:43 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:27:59:27:59 | IntegerLiteral | timestamp 2 | test_boolean.py:27:20:27:20 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:40:10:40:61 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:40:86:40:86 | IntegerLiteral | timestamp 3 | test_boolean.py:40:16:40:16 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:46:10:46:61 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:46:86:46:86 | IntegerLiteral | timestamp 3 | test_boolean.py:46:16:46:16 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:52:10:52:95 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:52:120:52:120 | IntegerLiteral | timestamp 4 | test_boolean.py:52:20:52:20 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:52:10:52:95 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:52:120:52:120 | IntegerLiteral | timestamp 4 | test_boolean.py:52:63:52:63 | IntegerLiteral | timestamp 2 |
+| test_boolean.py:52:11:52:47 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:52:63:52:63 | IntegerLiteral | timestamp 2 | test_boolean.py:52:20:52:20 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:64:10:64:52 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:64:59:64:59 | IntegerLiteral | timestamp 6 | test_boolean.py:64:17:64:17 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:64:10:64:52 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:64:59:64:59 | IntegerLiteral | timestamp 6 | test_boolean.py:64:27:64:27 | IntegerLiteral | timestamp 2 |
+| test_boolean.py:76:10:76:51 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:76:58:76:58 | IntegerLiteral | timestamp 6 | test_boolean.py:76:17:76:17 | IntegerLiteral | timestamp 0 |
+| test_boolean.py:76:10:76:51 | ControlFlowNode for BoolExpr | Basic block ordering: $@ appears before $@ | test_boolean.py:76:58:76:58 | IntegerLiteral | timestamp 6 | test_boolean.py:76:27:76:27 | IntegerLiteral | timestamp 2 |
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.ql
new file mode 100644
index 000000000000..6f40b9680906
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.ql
@@ -0,0 +1,17 @@
+/**
+ * Checks that within a single basic block, annotations appear in
+ * increasing minimum-timestamp order.
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from TimerCfgNode a, TimerCfgNode b, int minA, int minB
+where basicBlockOrdering(a, b, minA, minB)
+select a, "Basic block ordering: $@ appears before $@", a.getTimestampExpr(minA),
+  "timestamp " + minA, b.getTimestampExpr(minB), "timestamp " + minB

From 3f0cdcc405a76f516a6110e78e28e3100c517258 Mon Sep 17 00:00:00 2001
From: Taus <tausbn@github.com>
Date: Tue, 28 Apr 2026 15:07:04 +0000
Subject: [PATCH 4/5] Python: Add NeverReachable test

This looks for nodes annotated with `t[never]` in the test that are
reachable in the CFG. This should not happen (it messes with various
queries, e.g. the "mixed returns" query), but the test shows that in a
few particular cases (involving the `match` statement where all cases
contain `return`s), we _do_ have reachable nodes that shouldn't be.
---
 .../evaluation-order/NeverReachable.expected    |  2 ++
 .../evaluation-order/NeverReachable.ql          | 17 +++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.ql

diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.expected
new file mode 100644
index 000000000000..874a7dfb0960
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.expected
@@ -0,0 +1,2 @@
+| test_match.py:159:13:159:13 | IntegerLiteral | Node annotated with t.never is reachable in $@ | test_match.py:151:1:151:42 | Function test_match_exhaustive_return_first | test_match_exhaustive_return_first |
+| test_match.py:172:13:172:13 | IntegerLiteral | Node annotated with t.never is reachable in $@ | test_match.py:164:1:164:45 | Function test_match_exhaustive_return_wildcard | test_match_exhaustive_return_wildcard |
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.ql
new file mode 100644
index 000000000000..0ed7aab78d3d
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.ql
@@ -0,0 +1,17 @@
+/**
+ * Checks that expressions annotated with `t.never` either have no CFG
+ * node, or if they do, that the node is not reachable from its scope's
+ * entry (including within the same basic block).
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils::CfgTests
+
+from TimerAnnotation ann
+where neverReachable(ann)
+select ann, "Node annotated with t.never is reachable in $@", ann.getTestFunction(),
+  ann.getTestFunction().getName()

From c53bbdd1b9707e4078fa2ffbded8815a84241af4 Mon Sep 17 00:00:00 2001
From: Taus <tausbn@github.com>
Date: Tue, 28 Apr 2026 15:07:15 +0000
Subject: [PATCH 5/5] Python: Add ConsecutiveTimestamps test

This one is potentially a bit iffy -- it checks for a very powerful
property (that implies many of the other queries), but as the test
results show, it can produce false positives when there is in fact no
problem. We may want to get rid of it entirely, if it becomes too noisy.
---
 .../ConsecutiveTimestamps.expected            |  9 +++++++
 .../evaluation-order/ConsecutiveTimestamps.ql | 25 +++++++++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.expected
 create mode 100644 python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.ql

diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.expected
new file mode 100644
index 000000000000..e8071c044213
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.expected
@@ -0,0 +1,9 @@
+| test_boolean.py:9:26:9:27 | IntegerLiteral | $@ in $@ has no consecutive successor (expected 2) | test_boolean.py:9:33:9:33 | IntegerLiteral | Timestamp 1 | test_boolean.py:7:1:7:27 | Function test_and_both_sides | test_and_both_sides |
+| test_boolean.py:15:10:15:14 | False | $@ in $@ has no consecutive successor (expected 1) | test_boolean.py:15:20:15:20 | IntegerLiteral | Timestamp 0 | test_boolean.py:13:1:13:30 | Function test_and_short_circuit | test_and_short_circuit |
+| test_boolean.py:21:10:21:13 | True | $@ in $@ has no consecutive successor (expected 1) | test_boolean.py:21:19:21:19 | IntegerLiteral | Timestamp 0 | test_boolean.py:19:1:19:29 | Function test_or_short_circuit | test_or_short_circuit |
+| test_boolean.py:27:26:27:27 | IntegerLiteral | $@ in $@ has no consecutive successor (expected 2) | test_boolean.py:27:33:27:33 | IntegerLiteral | Timestamp 1 | test_boolean.py:25:1:25:26 | Function test_or_both_sides | test_or_both_sides |
+| test_boolean.py:40:45:40:45 | IntegerLiteral | $@ in $@ has no consecutive successor (expected 3) | test_boolean.py:40:51:40:51 | IntegerLiteral | Timestamp 2 | test_boolean.py:38:1:38:24 | Function test_chained_and | test_chained_and |
+| test_boolean.py:46:44:46:45 | IntegerLiteral | $@ in $@ has no consecutive successor (expected 3) | test_boolean.py:46:51:46:51 | IntegerLiteral | Timestamp 2 | test_boolean.py:44:1:44:23 | Function test_chained_or | test_chained_or |
+| test_boolean.py:52:11:52:47 | BoolExpr | $@ in $@ has no consecutive successor (expected 3) | test_boolean.py:52:63:52:63 | IntegerLiteral | Timestamp 2 | test_boolean.py:50:1:50:25 | Function test_mixed_and_or | test_mixed_and_or |
+| test_boolean.py:52:27:52:31 | False | $@ in $@ has no consecutive successor (expected 2) | test_boolean.py:52:37:52:37 | IntegerLiteral | Timestamp 1 | test_boolean.py:50:1:50:25 | Function test_mixed_and_or | test_mixed_and_or |
+| test_boolean.py:52:78:52:79 | IntegerLiteral | $@ in $@ has no consecutive successor (expected 4) | test_boolean.py:52:85:52:85 | IntegerLiteral | Timestamp 3 | test_boolean.py:50:1:50:25 | Function test_mixed_and_or | test_mixed_and_or |
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.ql
new file mode 100644
index 000000000000..e1871f81c207
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.ql
@@ -0,0 +1,25 @@
+/**
+ * Checks that consecutive annotated nodes have consecutive timestamps:
+ * for each annotation with timestamp `a`, some CFG node for that annotation
+ * must have a next annotation containing `a + 1`.
+ *
+ * Handles CFG splitting (e.g., finally blocks duplicated for normal/exceptional
+ * flow) by checking that at least one split has the required successor.
+ *
+ * Only applies to functions where all annotations are in the function's
+ * own scope (excludes tests with generators, async, comprehensions, or
+ * lambdas that have annotations in nested scopes).
+ */
+
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils
+private import Utils::CfgTests
+
+from TimerAnnotation ann, int a
+where consecutiveTimestamps(ann, a)
+select ann, "$@ in $@ has no consecutive successor (expected " + (a + 1) + ")",
+  ann.getTimestampExpr(a), "Timestamp " + a, ann.getTestFunction(), ann.getTestFunction().getName()