diff --git a/python/ql/lib/qlpack.yml b/python/ql/lib/qlpack.yml
index 8d8597ea9158..00dde24e2118 100644
--- a/python/ql/lib/qlpack.yml
+++ b/python/ql/lib/qlpack.yml
@@ -7,6 +7,7 @@ library: true
 upgrades: upgrades
 dependencies:
   codeql/concepts: ${workspace}
+  codeql/controlflow: ${workspace}
   codeql/dataflow: ${workspace}
   codeql/mad: ${workspace}
   codeql/regex: ${workspace}
diff --git a/python/ql/lib/semmle/python/controlflow/internal/AstNodeImpl.qll b/python/ql/lib/semmle/python/controlflow/internal/AstNodeImpl.qll
new file mode 100644
index 000000000000..c5e2d010688c
--- /dev/null
+++ b/python/ql/lib/semmle/python/controlflow/internal/AstNodeImpl.qll
@@ -0,0 +1,1294 @@
+/**
+ * Provides a newtype-based interface layer that mediates between the existing
+ * Python AST classes and the shared control-flow library's `AstSig` signature.
+ *
+ * The newtype unifies Python's `Stmt`, `Expr`, `Scope`, and `StmtList` into a
+ * single `AstNode` type. Notably, `StmtList` (which is not an `AstNode` in the
+ * existing Python AST) is wrapped as a `BlockStmt` (a subtype of `Stmt`),
+ * since the shared CFG library expects statement blocks to be statements.
+ */
+
+private import python as Py
+private import codeql.controlflow.ControlFlowGraph
+private import codeql.controlflow.SuccessorType
+
+private module Ast {
+  /** The newtype representing AST nodes for the shared CFG library. */
+  private newtype TAstNode =
+    TStmtNode(Py::Stmt s) or
+    TExprNode(Py::Expr e) or
+    TScopeNode(Py::Scope sc) or
+    TStmtListNode(Py::StmtList sl) or
+    /**
+     * A synthetic node representing an intermediate pair in a multi-operand
+     * `and`/`or` expression. For `a and b and c` (values 0,1,2), we
+     * synthesize a right-nested tree: the pair at index 1 represents
+     * `b and c`, which becomes the right operand of the outermost pair.
+     *
+     * Only created for inner pairs (index >= 1); the outermost pair (index 0)
+     * is represented by the original `BoolExpr` node via `TExprNode`.
+     */
+    TBoolExprPair(Py::BoolExpr be, int index) { index = [1 .. count(be.getAValue()) - 2] }
+
+  /**
+   * An AST node for the shared CFG. Each branch of the newtype gets a
+   * subclass that overrides `toString` and `getLocation`.
+   */
+  class Node extends TAstNode {
+    string toString() { none() }
+
+    Py::Location getLocation() { none() }
+
+    /** Gets the enclosing scope of this node, if any. */
+    ScopeNode getEnclosingScope() { none() }
+  }
+
+  class StmtNode extends Node, TStmtNode {
+    private Py::Stmt stmt;
+
+    StmtNode() { this = TStmtNode(stmt) }
+
+    /** Gets the underlying Python statement. */
+    Py::Stmt asStmt() { result = stmt }
+
+    override string toString() { result = stmt.toString() }
+
+    override Py::Location getLocation() { result = stmt.getLocation() }
+
+    /** Gets the enclosing scope of this statement. */
+    override ScopeNode getEnclosingScope() { result.asScope() = stmt.getScope() }
+  }
+
+  class ExprNode extends Node, TExprNode {
+    private Py::Expr expr;
+
+    ExprNode() { this = TExprNode(expr) }
+
+    /** Gets the underlying Python expression. */
+    Py::Expr asExpr() { result = expr }
+
+    override string toString() { result = expr.toString() }
+
+    override Py::Location getLocation() { result = expr.getLocation() }
+
+    /** Gets the enclosing scope of this expression. */
+    override ScopeNode getEnclosingScope() { result.asScope() = expr.getScope() }
+  }
+
+  class ScopeNode extends Node, TScopeNode {
+    private Py::Scope scope;
+
+    ScopeNode() { this = TScopeNode(scope) }
+
+    /** Gets the underlying Python scope. */
+    Py::Scope asScope() { result = scope }
+
+    override string toString() { result = scope.toString() }
+
+    override Py::Location getLocation() { result = scope.getLocation() }
+
+    /** Gets the body of this scope. */
+    StmtListNode getBody() { result.asStmtList() = scope.getBody() }
+
+    /** Gets the enclosing scope of this scope, if any. */
+    override ScopeNode getEnclosingScope() { result.asScope() = scope.getEnclosingScope() }
+  }
+
+  class StmtListNode extends Node, TStmtListNode {
+    private Py::StmtList stmtList;
+
+    StmtListNode() { this = TStmtListNode(stmtList) }
+
+    /** Gets the underlying Python statement list. */
+    Py::StmtList asStmtList() { result = stmtList }
+
+    override string toString() { result = stmtList.toString() }
+
+    // StmtList has no native location; approximate with first item's location.
+    override Py::Location getLocation() { result = stmtList.getItem(0).getLocation() }
+
+    /** Gets the `n`th (zero-based) statement in this block. */
+    StmtNode getItem(int n) { result.asStmt() = stmtList.getItem(n) }
+
+    /** Gets the last statement in this block. */
+    StmtNode getLastItem() { result.asStmt() = stmtList.getLastItem() }
+
+    /** Gets the enclosing scope of this statement list. */
+    override ScopeNode getEnclosingScope() {
+      result.asScope() = stmtList.getParent().(Py::Scope)
+      or
+      result.asScope() = stmtList.getParent().(Py::Stmt).getScope()
+    }
+  }
+
+  /** An `if` statement. */
+  class IfNode extends StmtNode {
+    private Py::If ifStmt;
+
+    IfNode() { ifStmt = this.asStmt() }
+
+    /** Gets the condition of this `if` statement. */
+    ExprNode getTest() { result.asExpr() = ifStmt.getTest() }
+
+    /** Gets the if-true branch. */
+    StmtListNode getBody() { result.asStmtList() = ifStmt.getBody() }
+
+    /** Gets the if-false branch, if any. */
+    StmtListNode getOrelse() { result.asStmtList() = ifStmt.getOrelse() }
+  }
+
+  /** An expression statement. */
+  class ExprStmtNode extends StmtNode {
+    private Py::ExprStmt exprStmt;
+
+    ExprStmtNode() { exprStmt = this.asStmt() }
+
+    /** Gets the expression in this statement. */
+    ExprNode getValue() { result.asExpr() = exprStmt.getValue() }
+  }
+
+  /** An assignment statement (`x = y = expr`). */
+  class AssignNode extends StmtNode {
+    private Py::Assign assign;
+
+    AssignNode() { assign = this.asStmt() }
+
+    ExprNode getValue() { result.asExpr() = assign.getValue() }
+
+    ExprNode getTarget(int n) { result.asExpr() = assign.getTarget(n) }
+
+    int getNumberOfTargets() { result = count(assign.getATarget()) }
+  }
+
+  /** An augmented assignment statement (`x += expr`). */
+  class AugAssignNode extends StmtNode {
+    private Py::AugAssign augAssign;
+
+    AugAssignNode() { augAssign = this.asStmt() }
+
+    ExprNode getOperation() { result.asExpr() = augAssign.getOperation() }
+  }
+
+  /** An assignment expression / walrus operator (`x := expr`). */
+  class AssignExprNode extends ExprNode {
+    private Py::AssignExpr assignExpr;
+
+    AssignExprNode() { assignExpr = this.asExpr() }
+
+    ExprNode getValue() { result.asExpr() = assignExpr.getValue() }
+
+    ExprNode getTarget() { result.asExpr() = assignExpr.getTarget() }
+  }
+
+  /** A `while` statement. */
+  class WhileNode extends StmtNode {
+    private Py::While whileStmt;
+
+    WhileNode() { whileStmt = this.asStmt() }
+
+    ExprNode getTest() { result.asExpr() = whileStmt.getTest() }
+
+    StmtListNode getBody() { result.asStmtList() = whileStmt.getBody() }
+
+    StmtListNode getOrelse() { result.asStmtList() = whileStmt.getOrelse() }
+  }
+
+  /** A `for` statement. */
+  class ForNode extends StmtNode {
+    private Py::For forStmt;
+
+    ForNode() { forStmt = this.asStmt() }
+
+    ExprNode getTarget() { result.asExpr() = forStmt.getTarget() }
+
+    ExprNode getIter() { result.asExpr() = forStmt.getIter() }
+
+    StmtListNode getBody() { result.asStmtList() = forStmt.getBody() }
+
+    StmtListNode getOrelse() { result.asStmtList() = forStmt.getOrelse() }
+  }
+
+  /** A `return` statement. */
+  class ReturnNode extends StmtNode {
+    private Py::Return ret;
+
+    ReturnNode() { ret = this.asStmt() }
+
+    ExprNode getValue() { result.asExpr() = ret.getValue() }
+  }
+
+  /** A `raise` statement. */
+  class RaiseNode extends StmtNode {
+    private Py::Raise raise;
+
+    RaiseNode() { raise = this.asStmt() }
+
+    ExprNode getException() { result.asExpr() = raise.getException() }
+
+    ExprNode getCause() { result.asExpr() = raise.getCause() }
+  }
+
+  /** A `with` statement. */
+  class WithNode extends StmtNode {
+    private Py::With withStmt;
+
+    WithNode() { withStmt = this.asStmt() }
+
+    ExprNode getContextExpr() { result.asExpr() = withStmt.getContextExpr() }
+
+    ExprNode getOptionalVars() { result.asExpr() = withStmt.getOptionalVars() }
+
+    StmtListNode getBody() { result.asStmtList() = withStmt.getBody() }
+  }
+
+  /** A `break` statement. */
+  class BreakNode extends StmtNode {
+    BreakNode() { this.asStmt() instanceof Py::Break }
+  }
+
+  /** A `continue` statement. */
+  class ContinueNode extends StmtNode {
+    ContinueNode() { this.asStmt() instanceof Py::Continue }
+  }
+
+  /** An `assert` statement. */
+  class AssertNode extends StmtNode {
+    private Py::Assert assertStmt;
+
+    AssertNode() { assertStmt = this.asStmt() }
+
+    ExprNode getTest() { result.asExpr() = assertStmt.getTest() }
+
+    ExprNode getMsg() { result.asExpr() = assertStmt.getMsg() }
+  }
+
+  /** A `delete` statement. */
+  class DeleteNode extends StmtNode {
+    private Py::Delete del;
+
+    DeleteNode() { del = this.asStmt() }
+
+    ExprNode getTarget(int n) { result.asExpr() = del.getTarget(n) }
+  }
+
+  /** A `match` statement. */
+  class MatchStmtNode extends StmtNode {
+    private Py::MatchStmt matchStmt;
+
+    MatchStmtNode() { matchStmt = this.asStmt() }
+
+    ExprNode getSubject() { result.asExpr() = matchStmt.getSubject() }
+
+    CaseNode getCase(int n) { result.asStmt() = matchStmt.getCase(n) }
+  }
+
+  /** A `case` clause in a match statement. */
+  class CaseNode extends StmtNode {
+    private Py::Case caseStmt;
+
+    CaseNode() { caseStmt = this.asStmt() }
+
+    ExprNode getGuard() { result.asExpr() = caseStmt.getGuard().(Py::Guard).getTest() }
+
+    StmtListNode getBody() { result.asStmtList() = caseStmt.getBody() }
+
+    predicate isWildcard() { caseStmt.getPattern() instanceof Py::MatchWildcardPattern }
+  }
+
+  /** A `try` statement. */
+  class TryNode extends StmtNode {
+    private Py::Try tryStmt;
+
+    TryNode() { tryStmt = this.asStmt() }
+
+    StmtListNode getBody() { result.asStmtList() = tryStmt.getBody() }
+
+    StmtListNode getOrelse() { result.asStmtList() = tryStmt.getOrelse() }
+
+    StmtListNode getFinalbody() { result.asStmtList() = tryStmt.getFinalbody() }
+
+    ExceptionHandlerNode getHandler(int i) { result.asStmt() = tryStmt.getHandler(i) }
+  }
+
+  /** An exception handler (`except` or `except*`). */
+  class ExceptionHandlerNode extends StmtNode {
+    private Py::ExceptionHandler handler;
+
+    ExceptionHandlerNode() { handler = this.asStmt() }
+
+    ExprNode getType() { result.asExpr() = handler.getType() }
+
+    ExprNode getName() { result.asExpr() = handler.getName() }
+
+    StmtListNode getBody() {
+      result.asStmtList() = handler.(Py::ExceptStmt).getBody() or
+      result.asStmtList() = handler.(Py::ExceptGroupStmt).getBody()
+    }
+  }
+
+  /** A conditional expression (`x if cond else y`). */
+  class IfExpNode extends ExprNode {
+    private Py::IfExp ifExp;
+
+    IfExpNode() { ifExp = this.asExpr() }
+
+    ExprNode getTest() { result.asExpr() = ifExp.getTest() }
+
+    ExprNode getBody() { result.asExpr() = ifExp.getBody() }
+
+    ExprNode getOrelse() { result.asExpr() = ifExp.getOrelse() }
+  }
+
+  /** A Python binary expression (arithmetic, bitwise, matmul, etc.). */
+  class BinaryExprNode extends ExprNode {
+    private Py::BinaryExpr binExpr;
+
+    BinaryExprNode() { binExpr = this.asExpr() }
+
+    ExprNode getLeft() { result.asExpr() = binExpr.getLeft() }
+
+    ExprNode getRight() { result.asExpr() = binExpr.getRight() }
+  }
+
+  /** A call expression (`func(args...)`). */
+  class CallNode extends ExprNode {
+    private Py::Call call;
+
+    CallNode() { call = this.asExpr() }
+
+    ExprNode getFunc() { result.asExpr() = call.getFunc() }
+
+    ExprNode getPositionalArg(int n) { result.asExpr() = call.getPositionalArg(n) }
+
+    int getNumberOfPositionalArgs() { result = count(call.getAPositionalArg()) }
+
+    ExprNode getKeywordValue(int n) {
+      result.asExpr() = call.getNamedArg(n).(Py::Keyword).getValue()
+      or
+      result.asExpr() = call.getNamedArg(n).(Py::DictUnpacking).getValue()
+    }
+
+    int getNumberOfNamedArgs() { result = count(call.getANamedArg()) }
+  }
+
+  /** A subscript expression (`obj[index]`). */
+  class SubscriptNode extends ExprNode {
+    private Py::Subscript sub;
+
+    SubscriptNode() { sub = this.asExpr() }
+
+    ExprNode getObject() { result.asExpr() = sub.getObject() }
+
+    ExprNode getIndex() { result.asExpr() = sub.getIndex() }
+  }
+
+  /** An attribute access (`obj.name`). */
+  class AttributeNode extends ExprNode {
+    private Py::Attribute attr;
+
+    AttributeNode() { attr = this.asExpr() }
+
+    ExprNode getObject() { result.asExpr() = attr.getObject() }
+  }
+
+  /** A tuple literal. */
+  class TupleNode extends ExprNode {
+    private Py::Tuple tuple;
+
+    TupleNode() { tuple = this.asExpr() }
+
+    ExprNode getElt(int n) { result.asExpr() = tuple.getElt(n) }
+  }
+
+  /** A list literal. */
+  class ListNode extends ExprNode {
+    private Py::List list;
+
+    ListNode() { list = this.asExpr() }
+
+    ExprNode getElt(int n) { result.asExpr() = list.getElt(n) }
+  }
+
+  /** A set literal. */
+  class SetNode extends ExprNode {
+    private Py::Set set;
+
+    SetNode() { set = this.asExpr() }
+
+    ExprNode getElt(int n) { result.asExpr() = set.getElt(n) }
+  }
+
+  /** A dict literal. */
+  class DictNode extends ExprNode {
+    private Py::Dict dict;
+
+    DictNode() { dict = this.asExpr() }
+
+    /**
+     * Gets the key of the `n`th item (at child index `2*n`), and the
+     * value at child index `2*n + 1`.
+     */
+    ExprNode getKey(int n) { result.asExpr() = dict.getItem(n).(Py::KeyValuePair).getKey() }
+
+    ExprNode getValue(int n) { result.asExpr() = dict.getItem(n).(Py::KeyValuePair).getValue() }
+
+    int getNumberOfItems() { result = count(dict.getAnItem()) }
+  }
+
+  /** A unary expression other than `not` (e.g., `-x`, `+x`, `~x`). */
+  class ArithmeticUnaryNode extends ExprNode {
+    private Py::UnaryExpr unaryExpr;
+
+    ArithmeticUnaryNode() { unaryExpr = this.asExpr() and not unaryExpr.getOp() instanceof Py::Not }
+
+    ExprNode getOperand() { result.asExpr() = unaryExpr.getOperand() }
+  }
+
+  /**
+   * A comprehension or generator expression.
+   * The iterable is evaluated in the enclosing scope; the body runs in a
+   * nested synthetic function scope handled by its own CFG.
+   */
+  class ComprehensionNode extends ExprNode {
+    private Py::Expr iterable;
+
+    ComprehensionNode() {
+      iterable = this.asExpr().(Py::ListComp).getIterable()
+      or
+      iterable = this.asExpr().(Py::SetComp).getIterable()
+      or
+      iterable = this.asExpr().(Py::DictComp).getIterable()
+      or
+      iterable = this.asExpr().(Py::GeneratorExp).getIterable()
+    }
+
+    ExprNode getIterable() { result.asExpr() = iterable }
+  }
+
+  /** A comparison expression (`a < b`, `a < b < c`, etc.). */
+  class CompareNode extends ExprNode {
+    private Py::Compare cmp;
+
+    CompareNode() { cmp = this.asExpr() }
+
+    ExprNode getLeft() { result.asExpr() = cmp.getLeft() }
+
+    ExprNode getComparator(int n) { result.asExpr() = cmp.getComparator(n) }
+  }
+
+  /** A slice expression (`start:stop:step`). */
+  class SliceNode extends ExprNode {
+    private Py::Slice slice;
+
+    SliceNode() { slice = this.asExpr() }
+
+    ExprNode getStart() { result.asExpr() = slice.getStart() }
+
+    ExprNode getStop() { result.asExpr() = slice.getStop() }
+
+    ExprNode getStep() { result.asExpr() = slice.getStep() }
+  }
+
+  /** A starred expression (`*x`). */
+  class StarredNode extends ExprNode {
+    private Py::Starred starred;
+
+    StarredNode() { starred = this.asExpr() }
+
+    ExprNode getValue() { result.asExpr() = starred.getValue() }
+  }
+
+  /** A formatted string literal (`f"...{expr}..."`). */
+  class FstringNode extends ExprNode {
+    private Py::Fstring fstring;
+
+    FstringNode() { fstring = this.asExpr() }
+
+    ExprNode getValue(int n) { result.asExpr() = fstring.getValue(n) }
+  }
+
+  /** A formatted value inside an f-string (`{expr}` or `{expr:spec}`). */
+  class FormattedValueNode extends ExprNode {
+    private Py::FormattedValue fv;
+
+    FormattedValueNode() { fv = this.asExpr() }
+
+    ExprNode getValue() { result.asExpr() = fv.getValue() }
+
+    ExprNode getFormatSpec() { result.asExpr() = fv.getFormatSpec() }
+  }
+
+  /** A `yield` expression. */
+  class YieldNode extends ExprNode {
+    private Py::Yield yield;
+
+    YieldNode() { yield = this.asExpr() }
+
+    ExprNode getValue() { result.asExpr() = yield.getValue() }
+  }
+
+  /** A `yield from` expression. */
+  class YieldFromNode extends ExprNode {
+    private Py::YieldFrom yieldFrom;
+
+    YieldFromNode() { yieldFrom = this.asExpr() }
+
+    ExprNode getValue() { result.asExpr() = yieldFrom.getValue() }
+  }
+
+  /** An `await` expression. */
+  class AwaitNode extends ExprNode {
+    private Py::Await await;
+
+    AwaitNode() { await = this.asExpr() }
+
+    ExprNode getValue() { result.asExpr() = await.getValue() }
+  }
+
+  /** A class definition expression (has base classes evaluated at definition time). */
+  class ClassExprNode extends ExprNode {
+    private Py::ClassExpr classExpr;
+
+    ClassExprNode() { classExpr = this.asExpr() }
+
+    ExprNode getBase(int n) { result.asExpr() = classExpr.getBase(n) }
+  }
+
+  /** A function definition expression (has default args evaluated at definition time). */
+  class FunctionExprNode extends ExprNode {
+    private Py::FunctionExpr funcExpr;
+
+    FunctionExprNode() { funcExpr = this.asExpr() }
+
+    ExprNode getDefault(int n) { result.asExpr() = funcExpr.getArgs().getDefault(n) }
+
+    ExprNode getKwDefault(int n) { result.asExpr() = funcExpr.getArgs().getKwDefault(n) }
+  }
+
+  /** A lambda expression (has default args evaluated at definition time). */
+  class LambdaNode extends ExprNode {
+    private Py::Lambda lambda;
+
+    LambdaNode() { lambda = this.asExpr() }
+
+    ExprNode getDefault(int n) { result.asExpr() = lambda.getArgs().getDefault(n) }
+
+    ExprNode getKwDefault(int n) { result.asExpr() = lambda.getArgs().getKwDefault(n) }
+  }
+
+  /**
+   * A `not` expression. This is a `UnaryExpr` whose operator is `Not`.
+   */
+  class NotExprNode extends ExprNode {
+    private Py::UnaryExpr notExpr;
+
+    NotExprNode() { notExpr = this.asExpr() and notExpr.getOp() instanceof Py::Not }
+
+    ExprNode getOperand() { result.asExpr() = notExpr.getOperand() }
+  }
+
+  /**
+   * A boolean expression (`and`/`or`) with exactly 2 operands.
+   * For 2-operand BoolExprs, the `TExprNode` itself serves as the
+   * logical and/or expression.
+   */
+  class BoolExpr2Node extends ExprNode {
+    private Py::BoolExpr boolExpr;
+
+    BoolExpr2Node() { boolExpr = this.asExpr() and count(boolExpr.getAValue()) = 2 }
+
+    predicate isAnd() { boolExpr.getOp() instanceof Py::And }
+
+    predicate isOr() { boolExpr.getOp() instanceof Py::Or }
+
+    ExprNode getLeftOperand() { result.asExpr() = boolExpr.getValue(0) }
+
+    ExprNode getRightOperand() { result.asExpr() = boolExpr.getValue(1) }
+  }
+
+  /**
+   * The outermost pair of a multi-operand (3+) boolean expression.
+   * Represented by the original `BoolExpr` node (`TExprNode`).
+   * Left operand is `getValue(0)`, right operand is `TBoolExprPair(be, 1)`.
+   */
+  class BoolExprOuterNode extends ExprNode {
+    private Py::BoolExpr boolExpr;
+
+    BoolExprOuterNode() { boolExpr = this.asExpr() and count(boolExpr.getAValue()) > 2 }
+
+    predicate isAnd() { boolExpr.getOp() instanceof Py::And }
+
+    predicate isOr() { boolExpr.getOp() instanceof Py::Or }
+
+    Node getLeftOperand() { result = TExprNode(boolExpr.getValue(0)) }
+
+    Node getRightOperand() { result = TBoolExprPair(boolExpr, 1) }
+  }
+
+  /**
+   * A synthetic intermediate node in a multi-operand boolean expression.
+   * Pair at index `i` has left=`getValue(i)` and right=pair at `i+1`
+   * (or `getValue(n-1)` for the last pair).
+   */
+  class BoolExprPairNode extends Node, TBoolExprPair {
+    private Py::BoolExpr boolExpr;
+    private int index;
+
+    BoolExprPairNode() { this = TBoolExprPair(boolExpr, index) }
+
+    override string toString() { result = boolExpr.getOperator() }
+
+    override Py::Location getLocation() { result = boolExpr.getValue(index).getLocation() }
+
+    override ScopeNode getEnclosingScope() {
+      result.asScope() = boolExpr.getValue(index).getScope()
+    }
+
+    predicate isAnd() { boolExpr.getOp() instanceof Py::And }
+
+    predicate isOr() { boolExpr.getOp() instanceof Py::Or }
+
+    Node getLeftOperand() { result = TExprNode(boolExpr.getValue(index)) }
+
+    Node getRightOperand() {
+      // Last pair: right operand is the final value
+      index = count(boolExpr.getAValue()) - 2 and
+      result = TExprNode(boolExpr.getValue(index + 1))
+      or
+      // Not last pair: right operand is the next synthetic pair
+      index < count(boolExpr.getAValue()) - 2 and
+      result = TBoolExprPair(boolExpr, index + 1)
+    }
+  }
+
+  /** A `True` or `False` literal. */
+  class BoolLiteralNode extends ExprNode {
+    BoolLiteralNode() { this.asExpr() instanceof Py::True or this.asExpr() instanceof Py::False }
+
+    boolean getBoolValue() {
+      this.asExpr() instanceof Py::True and result = true
+      or
+      this.asExpr() instanceof Py::False and result = false
+    }
+  }
+}
+
+/** Provides an implementation of the AST signature for Python. */
+module AstSigImpl implements AstSig<Py::Location> {
+  class AstNode = Ast::Node;
+
+  /** Gets the child of `n` at the specified (zero-based) index. */
+  AstNode getChild(AstNode n, int index) {
+    // IfStmt: condition (0), then branch (1), else branch (2)
+    exists(Ast::IfNode ifNode | ifNode = n |
+      index = 0 and result = ifNode.getTest()
+      or
+      index = 1 and result = ifNode.getBody()
+      or
+      index = 2 and result = ifNode.getOrelse()
+    )
+    or
+    // BlockStmt (StmtList): indexed statements
+    result = n.(Ast::StmtListNode).getItem(index)
+    or
+    // ExprStmt: the expression (0)
+    index = 0 and result = n.(Ast::ExprStmtNode).getValue()
+    or
+    // Assign: value (0), targets (1..n)
+    exists(Ast::AssignNode a | a = n |
+      index = 0 and result = a.getValue()
+      or
+      result = a.getTarget(index - 1) and index >= 1
+    )
+    or
+    // AugAssign: the operation (0)
+    index = 0 and result = n.(Ast::AugAssignNode).getOperation()
+    or
+    // AssignExpr (walrus :=): value (0), target (1)
+    exists(Ast::AssignExprNode ae | ae = n |
+      index = 0 and result = ae.getValue()
+      or
+      index = 1 and result = ae.getTarget()
+    )
+    or
+    // WhileStmt: condition (0), body (1)
+    // Note: Python while/else is not directly supported by the shared library.
+    exists(Ast::WhileNode w | w = n |
+      index = 0 and result = w.getTest()
+      or
+      index = 1 and result = w.getBody()
+    )
+    or
+    // ForStmt (mapped as ForeachStmt): collection (0), variable (1), body (2)
+    exists(Ast::ForNode f | f = n |
+      index = 0 and result = f.getIter()
+      or
+      index = 1 and result = f.getTarget()
+      or
+      index = 2 and result = f.getBody()
+    )
+    or
+    // ReturnStmt: the value (0)
+    index = 0 and result = n.(Ast::ReturnNode).getValue()
+    or
+    // Assert: test (0), message (1)
+    exists(Ast::AssertNode a | a = n |
+      index = 0 and result = a.getTest()
+      or
+      index = 1 and result = a.getMsg()
+    )
+    or
+    // Delete: targets left to right
+    result = n.(Ast::DeleteNode).getTarget(index)
+    or
+    // With: context expr (0), optional vars (1), body (2)
+    exists(Ast::WithNode w | w = n |
+      index = 0 and result = w.getContextExpr()
+      or
+      index = 1 and result = w.getOptionalVars()
+      or
+      index = 2 and result = w.getBody()
+    )
+    or
+    // ThrowStmt (raise): the exception (0), the cause (1)
+    exists(Ast::RaiseNode r | r = n |
+      index = 0 and result = r.getException()
+      or
+      index = 1 and result = r.getCause()
+    )
+    or
+    // TryStmt: body (0), handlers (1..n), finally (-1)
+    exists(Ast::TryNode t | t = n |
+      index = 0 and result = t.getBody()
+      or
+      result = t.getHandler(index - 1) and index >= 1
+      or
+      index = -1 and result = t.getFinalbody()
+    )
+    or
+    // MatchStmt: subject (0), cases (1..n)
+    exists(Ast::MatchStmtNode m | m = n |
+      index = 0 and result = m.getSubject()
+      or
+      result = m.getCase(index - 1) and index >= 1
+    )
+    or
+    // Case: guard (0), body (1)
+    exists(Ast::CaseNode c | c = n |
+      index = 0 and result = c.getGuard()
+      or
+      index = 1 and result = c.getBody()
+    )
+    or
+    // CatchClause (except handler): type (0), name (1), body (2)
+    exists(Ast::ExceptionHandlerNode h | h = n |
+      index = 0 and result = h.getType()
+      or
+      index = 1 and result = h.getName()
+      or
+      index = 2 and result = h.getBody()
+    )
+    or
+    // ConditionalExpr (IfExp): condition (0), then (1), else (2)
+    exists(Ast::IfExpNode ie | ie = n |
+      index = 0 and result = ie.getTest()
+      or
+      index = 1 and result = ie.getBody()
+      or
+      index = 2 and result = ie.getOrelse()
+    )
+    or
+    // Call: func (0), positional args (1..n), keyword values (n+1..n+k)
+    exists(Ast::CallNode call | call = n |
+      index = 0 and result = call.getFunc()
+      or
+      result = call.getPositionalArg(index - 1) and index >= 1
+      or
+      result = call.getKeywordValue(index - 1 - call.getNumberOfPositionalArgs()) and
+      index >= 1 + call.getNumberOfPositionalArgs()
+    )
+    or
+    // Python BinaryExpr (arithmetic, bitwise, matmul, etc.): left (0), right (1)
+    exists(Ast::BinaryExprNode be | be = n |
+      index = 0 and result = be.getLeft()
+      or
+      index = 1 and result = be.getRight()
+    )
+    or
+    // Subscript (obj[index]): object (0), index (1)
+    exists(Ast::SubscriptNode sub | sub = n |
+      index = 0 and result = sub.getObject()
+      or
+      index = 1 and result = sub.getIndex()
+    )
+    or
+    // Attribute (obj.name): object (0)
+    index = 0 and result = n.(Ast::AttributeNode).getObject()
+    or
+    // Comprehension/generator: iterable (0)
+    index = 0 and result = n.(Ast::ComprehensionNode).getIterable()
+    or
+    // Tuple, List, Set: elements left to right
+    result = n.(Ast::TupleNode).getElt(index)
+    or
+    result = n.(Ast::ListNode).getElt(index)
+    or
+    result = n.(Ast::SetNode).getElt(index)
+    or
+    // Dict: key(0), value(0), key(1), value(1), ...
+    exists(Ast::DictNode d, int item | d = n |
+      index = 2 * item and result = d.getKey(item)
+      or
+      index = 2 * item + 1 and result = d.getValue(item)
+    )
+    or
+    // Arithmetic unary (-x, +x, ~x): operand (0)
+    index = 0 and result = n.(Ast::ArithmeticUnaryNode).getOperand()
+    or
+    // Compare (a < b < c): left (0), comparators (1..n)
+    exists(Ast::CompareNode cmp | cmp = n |
+      index = 0 and result = cmp.getLeft()
+      or
+      result = cmp.getComparator(index - 1) and index >= 1
+    )
+    or
+    // Slice (start:stop:step): start (0), stop (1), step (2)
+    exists(Ast::SliceNode sl | sl = n |
+      index = 0 and result = sl.getStart()
+      or
+      index = 1 and result = sl.getStop()
+      or
+      index = 2 and result = sl.getStep()
+    )
+    or
+    // Starred (*x): value (0)
+    index = 0 and result = n.(Ast::StarredNode).getValue()
+    or
+    // Fstring: values left to right
+    result = n.(Ast::FstringNode).getValue(index)
+    or
+    // FormattedValue ({expr} or {expr:spec}): value (0), format spec (1)
+    exists(Ast::FormattedValueNode fv | fv = n |
+      index = 0 and result = fv.getValue()
+      or
+      index = 1 and result = fv.getFormatSpec()
+    )
+    or
+    // Yield: value (0)
+    index = 0 and result = n.(Ast::YieldNode).getValue()
+    or
+    // YieldFrom: value (0)
+    index = 0 and result = n.(Ast::YieldFromNode).getValue()
+    or
+    // Await: value (0)
+    index = 0 and result = n.(Ast::AwaitNode).getValue()
+    or
+    // ClassExpr: base classes left to right
+    result = n.(Ast::ClassExprNode).getBase(index)
+    or
+    // FunctionExpr: defaults left to right, then kw defaults
+    exists(Ast::FunctionExprNode fe | fe = n |
+      result = fe.getDefault(index)
+      or
+      result =
+        fe.getKwDefault(index -
+            count(Py::Expr d | d = fe.asExpr().(Py::FunctionExpr).getArgs().getADefault()))
+    )
+    or
+    // Lambda: defaults left to right, then kw defaults
+    exists(Ast::LambdaNode lam | lam = n |
+      result = lam.getDefault(index)
+      or
+      result =
+        lam.getKwDefault(index -
+            count(Py::Expr d | d = lam.asExpr().(Py::Lambda).getArgs().getADefault()))
+    )
+    or
+    // LogicalNotExpr: operand (0)
+    index = 0 and result = n.(Ast::NotExprNode).getOperand()
+    or
+    // 2-operand BoolExpr: left (0), right (1)
+    exists(Ast::BoolExpr2Node be | be = n |
+      index = 0 and result = be.getLeftOperand()
+      or
+      index = 1 and result = be.getRightOperand()
+    )
+    or
+    // Multi-operand BoolExpr (outermost): left (0), right (1)
+    exists(Ast::BoolExprOuterNode be | be = n |
+      index = 0 and result = be.getLeftOperand()
+      or
+      index = 1 and result = be.getRightOperand()
+    )
+    or
+    // Synthetic BoolExpr pair: left (0), right (1)
+    exists(Ast::BoolExprPairNode bp | bp = n |
+      index = 0 and result = bp.getLeftOperand()
+      or
+      index = 1 and result = bp.getRightOperand()
+    )
+  }
+
+  Callable getEnclosingCallable(AstNode node) { result = node.getEnclosingScope() }
+
+  /**
+   * A callable: a function, class, or module scope.
+   *
+   * In Python, all three are executable scopes with statement bodies.
+   */
+  class Callable extends Ast::ScopeNode { }
+
+  /** Gets the body of callable `c`. */
+  AstNode callableGetBody(Callable c) { result = c.getBody() }
+
+  /** A statement. Includes both wrapped `Stmt` nodes and `StmtList` blocks. */
+  class Stmt extends AstNode {
+    Stmt() { this instanceof Ast::StmtNode or this instanceof Ast::StmtListNode }
+  }
+
+  /** An expression. Includes `TExprNode` and synthetic `TBoolExprPair` nodes. */
+  class Expr extends AstNode {
+    Expr() { this instanceof Ast::ExprNode or this instanceof Ast::BoolExprPairNode }
+  }
+
+  /** A block of statements, wrapping Python's `StmtList`. */
+  class BlockStmt extends Stmt, Ast::StmtListNode {
+    /** Gets the `n`th (zero-based) statement in this block. */
+    Stmt getStmt(int n) { result = Ast::StmtListNode.super.getItem(n) }
+
+    /** Gets the last statement in this block. */
+    Stmt getLastStmt() { result = Ast::StmtListNode.super.getLastItem() }
+  }
+
+  /** An expression statement. */
+  class ExprStmt extends Stmt, Ast::ExprStmtNode {
+    /** Gets the expression in this expression statement. */
+    Expr getExpr() { result = this.getValue() }
+  }
+
+  /**
+   * An `if` statement.
+   *
+   * Python's `elif` chains are represented as nested `If` nodes in the
+   * else branch's `StmtList`. The shared CFG library handles this naturally:
+   * `getElse()` returns the `BlockStmt` wrapping the else branch, and if that
+   * block contains a single `If`, the result is a chained conditional.
+   */
+  class IfStmt extends Stmt, Ast::IfNode {
+    /** Gets the condition of this `if` statement. */
+    Expr getCondition() { result = this.getTest() }
+
+    /** Gets the `then` (true) branch of this `if` statement. */
+    Stmt getThen() { result = Ast::IfNode.super.getBody() }
+
+    /** Gets the `else` (false) branch of this `if` statement, if any. */
+    Stmt getElse() { result = this.getOrelse() }
+  }
+
+  // ===== Loop statements =====
+  /** A loop statement. */
+  class LoopStmt extends Stmt {
+    LoopStmt() { this instanceof Ast::WhileNode or this instanceof Ast::ForNode }
+
+    /** Gets the body of this loop statement. */
+    Stmt getBody() { none() }
+  }
+
+  /** A `while` loop statement. */
+  class WhileStmt extends LoopStmt instanceof Ast::WhileNode {
+    /** Gets the boolean condition of this `while` loop. */
+    Expr getCondition() { result = this.(Ast::WhileNode).getTest() }
+
+    override Stmt getBody() { result = this.(Ast::WhileNode).getBody() }
+  }
+
+  /** A `do-while` loop statement. Python has no do-while construct. */
+  class DoStmt extends LoopStmt {
+    DoStmt() { none() }
+
+    Expr getCondition() { none() }
+  }
+
+  /** A C-style `for` loop. Python has no C-style for loop. */
+  class ForStmt extends LoopStmt {
+    ForStmt() { none() }
+
+    Expr getInit(int index) { none() }
+
+    Expr getCondition() { none() }
+
+    Expr getUpdate(int index) { none() }
+  }
+
+  /** A for-each loop (`for x in iterable:`). */
+  class ForeachStmt extends LoopStmt {
+    ForeachStmt() { this instanceof Ast::ForNode }
+
+    /** Gets the loop variable. */
+    Expr getVariable() { result = this.(Ast::ForNode).getTarget() }
+
+    /** Gets the collection being iterated. */
+    Expr getCollection() { result = this.(Ast::ForNode).getIter() }
+
+    override Stmt getBody() { result = this.(Ast::ForNode).getBody() }
+  }
+
+  // ===== Abrupt completion statements =====
+  /** A `break` statement. */
+  class BreakStmt extends Stmt, Ast::BreakNode { }
+
+  /** A `continue` statement. */
+  class ContinueStmt extends Stmt, Ast::ContinueNode { }
+
+  /** A `return` statement. */
+  class ReturnStmt extends Stmt, Ast::ReturnNode {
+    /** Gets the expression being returned, if any. */
+    Expr getExpr() { result = this.getValue() }
+  }
+
+  /** A `raise` statement (mapped to `ThrowStmt`). */
+  class ThrowStmt extends Stmt, Ast::RaiseNode {
+    /** Gets the expression being raised. */
+    Expr getExpr() { result = this.getException() }
+  }
+
+  // ===== Try/except =====
+  /** A `try` statement. */
+  class TryStmt extends Stmt {
+    TryStmt() { this instanceof Ast::TryNode }
+
+    Stmt getBody() { result = this.(Ast::TryNode).getBody() }
+
+    CatchClause getCatch(int index) { result = this.(Ast::TryNode).getHandler(index) }
+
+    Stmt getFinally() { result = this.(Ast::TryNode).getFinalbody() }
+  }
+
+  AstNode getTryElse(TryStmt try) { result = try.(Ast::TryNode).getOrelse() }
+
+  /** An except clause in a try statement. */
+  class CatchClause extends Stmt {
+    CatchClause() { this instanceof Ast::ExceptionHandlerNode }
+
+    AstNode getVariable() { result = this.(Ast::ExceptionHandlerNode).getName() }
+
+    Expr getCondition() { none() }
+
+    Stmt getBody() { result = this.(Ast::ExceptionHandlerNode).getBody() }
+  }
+
+  // ===== Switch/match =====
+  /** A `match` statement, mapped to the shared CFG's `Switch`. */
+  class Switch extends Stmt {
+    Switch() { this instanceof Ast::MatchStmtNode }
+
+    Expr getExpr() { result = this.(Ast::MatchStmtNode).getSubject() }
+
+    Case getCase(int index) { result = this.(Ast::MatchStmtNode).getCase(index) }
+
+    Stmt getStmt(int index) { none() }
+  }
+
+  /** A `case` clause in a match statement. */
+  class Case extends Stmt {
+    Case() { this instanceof Ast::CaseNode }
+
+    AstNode getAPattern() { none() }
+
+    Expr getGuard() { result = this.(Ast::CaseNode).getGuard() }
+
+    AstNode getBody() { result = this.(Ast::CaseNode).getBody() }
+  }
+
+  /** A wildcard case (`case _:`). */
+  class DefaultCase extends Case {
+    DefaultCase() { this.(Ast::CaseNode).isWildcard() }
+  }
+
+  // ===== Expression types =====
+  /** A conditional expression (`x if cond else y`). */
+  class ConditionalExpr extends Expr, Ast::IfExpNode {
+    /** Gets the condition of this expression. */
+    Expr getCondition() { result = this.getTest() }
+
+    /** Gets the true branch of this expression. */
+    Expr getThen() { result = Ast::IfExpNode.super.getBody() }
+
+    /** Gets the false branch of this expression. */
+    Expr getElse() { result = this.getOrelse() }
+  }
+
+  /**
+   * A binary expression for the shared CFG. In Python, this covers
+   * `and`/`or` expressions (both real 2-operand and synthetic pairs).
+   */
+  class BinaryExpr extends Expr {
+    BinaryExpr() {
+      this instanceof Ast::BoolExpr2Node or
+      this instanceof Ast::BoolExprOuterNode or
+      this instanceof Ast::BoolExprPairNode
+    }
+
+    /** Gets the left operand. */
+    Expr getLeftOperand() {
+      result = this.(Ast::BoolExpr2Node).getLeftOperand()
+      or
+      result = this.(Ast::BoolExprOuterNode).getLeftOperand()
+      or
+      result = this.(Ast::BoolExprPairNode).getLeftOperand()
+    }
+
+    /** Gets the right operand. */
+    Expr getRightOperand() {
+      result = this.(Ast::BoolExpr2Node).getRightOperand()
+      or
+      result = this.(Ast::BoolExprOuterNode).getRightOperand()
+      or
+      result = this.(Ast::BoolExprPairNode).getRightOperand()
+    }
+  }
+
+  /** A short-circuiting logical `and` expression. */
+  class LogicalAndExpr extends BinaryExpr {
+    LogicalAndExpr() {
+      this.(Ast::BoolExpr2Node).isAnd() or
+      this.(Ast::BoolExprOuterNode).isAnd() or
+      this.(Ast::BoolExprPairNode).isAnd()
+    }
+  }
+
+  /** A short-circuiting logical `or` expression. */
+  class LogicalOrExpr extends BinaryExpr {
+    LogicalOrExpr() {
+      this.(Ast::BoolExpr2Node).isOr() or
+      this.(Ast::BoolExprOuterNode).isOr() or
+      this.(Ast::BoolExprPairNode).isOr()
+    }
+  }
+
+  /** A null-coalescing expression. Python has no null-coalescing operator. */
+  class NullCoalescingExpr extends BinaryExpr {
+    NullCoalescingExpr() { none() }
+  }
+
+  /** A unary expression. Exists for the `not` subclass. */
+  class UnaryExpr extends Expr {
+    UnaryExpr() { this instanceof Ast::NotExprNode }
+
+    Expr getOperand() { result = this.(Ast::NotExprNode).getOperand() }
+  }
+
+  /** A logical `not` expression. */
+  class LogicalNotExpr extends UnaryExpr { }
+
+  /** A boolean literal expression (`True` or `False`). */
+  class BooleanLiteral extends Expr, Ast::BoolLiteralNode {
+    /** Gets the boolean value of this literal. */
+    boolean getValue() { result = this.getBoolValue() }
+  }
+}
+
+private module Cfg0 = Make0<Py::Location, AstSigImpl>;
+
+private import Cfg0
+
+private module Cfg1 = Make1<Input>;
+
+private import Cfg1
+
+private module Cfg2 = Make2<Input>;
+
+private import Cfg2
+
+private module Input implements InputSig1, InputSig2 {
+  predicate cfgCachedStageRef() { CfgCachedStage::ref() }
+
+  private newtype TLabel = TNone()
+
+  class Label extends TLabel {
+    string toString() { result = "label" }
+  }
+
+  predicate inConditionalContext(AstSigImpl::AstNode n, ConditionKind kind) {
+    kind.isBoolean() and
+    n = any(Ast::AssertNode a).getTest()
+  }
+
+  private string assertThrowTag() { result = "[assert-throw]" }
+
+  predicate additionalNode(AstSigImpl::AstNode n, string tag, NormalSuccessor t) {
+    n instanceof Ast::AssertNode and tag = assertThrowTag() and t instanceof DirectSuccessor
+  }
+
+  predicate beginAbruptCompletion(
+    AstSigImpl::AstNode ast, PreControlFlowNode n, AbruptCompletion c, boolean always
+  ) {
+    ast instanceof Ast::AssertNode and
+    n.isAdditional(ast, assertThrowTag()) and
+    c.asSimpleAbruptCompletion() instanceof ExceptionSuccessor and
+    always = true
+  }
+
+  predicate endAbruptCompletion(AstSigImpl::AstNode ast, PreControlFlowNode n, AbruptCompletion c) {
+    none()
+  }
+
+  predicate step(PreControlFlowNode n1, PreControlFlowNode n2) {
+    exists(Ast::AssertNode assertStmt |
+      n1.isBefore(assertStmt) and
+      n2.isBefore(assertStmt.getTest())
+      or
+      n1.isAfterTrue(assertStmt.getTest()) and
+      n2.isAfter(assertStmt)
+      or
+      n1.isAfterFalse(assertStmt.getTest()) and
+      (
+        n2.isBefore(assertStmt.getMsg())
+        or
+        not exists(assertStmt.getMsg()) and
+        n2.isAdditional(assertStmt, assertThrowTag())
+      )
+      or
+      n1.isAfter(assertStmt.getMsg()) and
+      n2.isAdditional(assertStmt, assertThrowTag())
+    )
+    or
+    // While/else: when the condition is false, flow to the else block
+    // (if present) before the after-while node.
+    exists(Ast::WhileNode w, Ast::StmtListNode orelse | orelse = w.getOrelse() |
+      n1.isAfterFalse(w.getTest()) and
+      n2.isBefore(orelse)
+      or
+      n1.isAfter(orelse) and
+      n2.isAfter(w)
+    )
+    or
+    // For/else: when the collection is empty or the loop completes normally,
+    // flow through the else block before the after-for node.
+    exists(Ast::ForNode f, Ast::StmtListNode orelse | orelse = f.getOrelse() |
+      n1.isAfterValue(f.getIter(), any(EmptinessSuccessor t | t.getValue() = true)) and
+      n2.isBefore(orelse)
+      or
+      n1.isAfter(f.getBody()) and
+      n2.isBefore(orelse)
+      or
+      n1.isAfter(orelse) and
+      n2.isAfter(f)
+    )
+  }
+}
+
+import CfgCachedStage
+import Public
+
+/**
+ * Maps a new-CFG AST wrapper node to the corresponding Python AST node, if any.
+ * Entry, exit, and synthetic nodes have no corresponding Python AST node.
+ */
+Py::AstNode astNodeToPyNode(AstSigImpl::AstNode n) {
+  result = n.(Ast::ExprNode).asExpr()
+  or
+  result = n.(Ast::StmtNode).asStmt()
+  or
+  result = n.(Ast::ScopeNode).asScope()
+}
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..de44daa3e2c2
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql
@@ -0,0 +1,19 @@
+/**
+ * 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 python
+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..5311d118576b
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/AnnotationHasCfgNode.ql
@@ -0,0 +1,16 @@
+/**
+ * Checks that every timer annotation has a corresponding CFG node.
+ */
+
+import python
+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..0a2b08ff3fdd
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql
@@ -0,0 +1,23 @@
+/**
+ * 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 python
+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/BasicBlockOrdering.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.expected
new file mode 100644
index 000000000000..573094ddf734
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.expected
@@ -0,0 +1 @@
+| test_comprehensions.py:21:29:21:40 | ControlFlowNode for BinaryExpr | Basic block ordering: $@ appears before $@ | test_comprehensions.py:21:35:21:35 | IntegerLiteral | timestamp 9 | test_comprehensions.py:21:21:21:21 | IntegerLiteral | timestamp 8 |
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..30697f1403e2
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockOrdering.ql
@@ -0,0 +1,18 @@
+/**
+ * Checks that within a single basic block, annotations appear in
+ * increasing minimum-timestamp order.
+ */
+
+import python
+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
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..e20e20c464d4
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.expected
@@ -0,0 +1 @@
+| test_if.py:51:9:51:16 | BinaryExpr | $@ in $@ has no consecutive successor (expected 6) | test_if.py:51:15:51:15 | IntegerLiteral | Timestamp 5 | test_if.py:43:1:43:31 | Function test_if_elif_else_first | test_if_elif_else_first |
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..709fd5665ea4
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.ql
@@ -0,0 +1,26 @@
+/**
+ * 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 python
+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()
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..456ebf447dad
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql
@@ -0,0 +1,18 @@
+/**
+ * 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 python
+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/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/NeverReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.expected
new file mode 100644
index 000000000000..200ebdbc6a74
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.expected
@@ -0,0 +1,2 @@
+| test_match.py:159:13:159:23 | BinaryExpr | 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:23 | BinaryExpr | 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..db55c1d92e4b
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NeverReachable.ql
@@ -0,0 +1,18 @@
+/**
+ * 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 python
+import TimerUtils
+import OldCfgImpl
+
+private module Utils = EvalOrderCfgUtils<OldCfg>;
+
+private import Utils::CfgTests
+
+from NeverTimerAnnotation ann
+where neverReachable(ann)
+select ann, "Node annotated with t.never is reachable in $@", ann.getTestFunction(),
+  ann.getTestFunction().getName()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAllLiveReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAllLiveReachable.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAllLiveReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAllLiveReachable.ql
new file mode 100644
index 000000000000..75f02d14a9cb
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAllLiveReachable.ql
@@ -0,0 +1,14 @@
+/** New-CFG version of AllLiveReachable. */
+
+import python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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/NewCfgAnnotationHasCfgNode.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAnnotationHasCfgNode.expected
new file mode 100644
index 000000000000..8b137891791f
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAnnotationHasCfgNode.expected
@@ -0,0 +1 @@
+
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAnnotationHasCfgNode.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAnnotationHasCfgNode.ql
new file mode 100644
index 000000000000..4b1d82e27e67
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgAnnotationHasCfgNode.ql
@@ -0,0 +1,18 @@
+/**
+ * New-CFG version of AnnotationHasCfgNode.
+ *
+ * Checks that every timer annotation has a corresponding CFG node.
+ */
+
+import python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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/NewCfgBasicBlockAnnotationGap.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockAnnotationGap.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockAnnotationGap.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockAnnotationGap.ql
new file mode 100644
index 000000000000..80dd759a3651
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockAnnotationGap.ql
@@ -0,0 +1,26 @@
+/**
+ * New-CFG version of BasicBlockAnnotationGap.
+ *
+ * Original:
+ * 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 python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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/NewCfgBasicBlockOrdering.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockOrdering.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockOrdering.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockOrdering.ql
new file mode 100644
index 000000000000..f06d08d937e3
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgBasicBlockOrdering.ql
@@ -0,0 +1,21 @@
+/**
+ * New-CFG version of BasicBlockOrdering.
+ *
+ * Original:
+ * Checks that within a single basic block, annotations appear in
+ * increasing minimum-timestamp order.
+ */
+
+import python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgConsecutiveTimestamps.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgConsecutiveTimestamps.expected
new file mode 100644
index 000000000000..bce948bb58a5
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgConsecutiveTimestamps.expected
@@ -0,0 +1 @@
+| test_if.py:51:9:51:9 | IntegerLiteral | $@ in $@ has no consecutive successor (expected 6) | test_if.py:51:15:51:15 | IntegerLiteral | Timestamp 5 | test_if.py:43:1:43:31 | Function test_if_elif_else_first | test_if_elif_else_first |
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgConsecutiveTimestamps.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgConsecutiveTimestamps.ql
new file mode 100644
index 000000000000..8e52663d6eaf
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgConsecutiveTimestamps.ql
@@ -0,0 +1,29 @@
+/**
+ * New-CFG version of ConsecutiveTimestamps.
+ *
+ * Original:
+ * 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 python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgImpl.qll b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgImpl.qll
new file mode 100644
index 000000000000..97c6a9c043fa
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgImpl.qll
@@ -0,0 +1,86 @@
+/**
+ * Implementation of the evaluation-order CFG signature using the new
+ * shared control flow graph from AstNodeImpl.
+ */
+
+private import python as Py
+import TimerUtils
+private import semmle.python.controlflow.internal.AstNodeImpl as CfgImpl
+
+private class NewControlFlowNode = CfgImpl::ControlFlowNode;
+
+private class NewBasicBlock = CfgImpl::BasicBlock;
+
+/** New (shared) CFG implementation of the evaluation-order signature. */
+module NewCfg implements EvalOrderCfgSig {
+  class CfgNode instanceof NewControlFlowNode {
+    // Use the post-order representative for each AST node: the "after" node.
+    // For simple leaf nodes this is the merged before/after node. For
+    // post-order expressions this is the TAstNode. For pre-order expressions
+    // (and/or/not/ternary) this uses an AfterValueNode, which places the
+    // expression after its operands — matching the timer test expectations.
+    CfgNode() { NewControlFlowNode.super.isAfter(_) }
+
+    string toString() { result = NewControlFlowNode.super.toString() }
+
+    Py::Location getLocation() { result = NewControlFlowNode.super.getLocation() }
+
+    Py::AstNode getNode() {
+      result = CfgImpl::astNodeToPyNode(NewControlFlowNode.super.getAstNode())
+    }
+
+    CfgNode getASuccessor() { nextCfgNode(this, result) }
+
+    CfgNode getAnExceptionalSuccessor() {
+      exists(NewControlFlowNode mid |
+        mid = NewControlFlowNode.super.getAnExceptionSuccessor() and
+        nextCfgNodeFrom(mid, result)
+      )
+    }
+
+    Py::Scope getScope() { result = NewControlFlowNode.super.getEnclosingCallable().asScope() }
+
+    BasicBlock getBasicBlock() {
+      exists(NewBasicBlock bb, int i | bb.getNode(i) = this and result = bb)
+    }
+  }
+
+  /**
+   * Holds if `next` is the nearest CfgNode reachable from `n` via
+   * one or more raw CFG successor edges, skipping non-CfgNode intermediaries.
+   */
+  private predicate nextCfgNodeFrom(NewControlFlowNode n, CfgNode next) {
+    next = n.getASuccessor()
+    or
+    exists(NewControlFlowNode mid |
+      mid = n.getASuccessor() and
+      not mid instanceof CfgNode and
+      nextCfgNodeFrom(mid, next)
+    )
+  }
+
+  /**
+   * Holds if `next` is the nearest CfgNode successor of `n`,
+   * skipping synthetic intermediate nodes.
+   */
+  private predicate nextCfgNode(CfgNode n, CfgNode next) { nextCfgNodeFrom(n, next) }
+
+  class BasicBlock instanceof NewBasicBlock {
+    string toString() { result = NewBasicBlock.super.toString() }
+
+    CfgNode getNode(int n) { result = NewBasicBlock.super.getNode(n) }
+
+    predicate reaches(BasicBlock bb) { this = bb or this.strictlyReaches(bb) }
+
+    predicate strictlyReaches(BasicBlock bb) { NewBasicBlock.super.getASuccessor+() = bb }
+
+    predicate strictlyDominates(BasicBlock bb) { NewBasicBlock.super.strictlyDominates(bb) }
+  }
+
+  CfgNode scopeGetEntryNode(Py::Scope s) {
+    exists(CfgImpl::ControlFlow::EntryNode entry |
+      entry.getEnclosingCallable().asScope() = s and
+      nextCfgNodeFrom(entry, result)
+    )
+  }
+}
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNeverReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNeverReachable.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNeverReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNeverReachable.ql
new file mode 100644
index 000000000000..3430d49b57ef
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNeverReachable.ql
@@ -0,0 +1,21 @@
+/**
+ * New-CFG version of NeverReachable.
+ *
+ * Original:
+ * 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 python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+private import Utils::CfgTests
+
+from NeverTimerAnnotation ann
+where neverReachable(ann)
+select ann, "Node annotated with t.never is reachable in $@", ann.getTestFunction(),
+  ann.getTestFunction().getName()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBackwardFlow.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBackwardFlow.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBackwardFlow.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBackwardFlow.ql
new file mode 100644
index 000000000000..442ca5f5456c
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBackwardFlow.ql
@@ -0,0 +1,22 @@
+/**
+ * New-CFG version of NoBackwardFlow.
+ *
+ * Original:
+ * 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 python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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/NewCfgNoBasicBlock.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBasicBlock.expected
new file mode 100644
index 000000000000..8b137891791f
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBasicBlock.expected
@@ -0,0 +1 @@
+
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBasicBlock.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBasicBlock.ql
new file mode 100644
index 000000000000..e07890f72502
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoBasicBlock.ql
@@ -0,0 +1,18 @@
+/**
+ * New-CFG version of NoBasicBlock.
+ *
+ * Checks that every annotated CFG node belongs to a basic block.
+ */
+
+import python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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/NewCfgNoSharedReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoSharedReachable.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoSharedReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoSharedReachable.ql
new file mode 100644
index 000000000000..5a1a1aba2a7a
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgNoSharedReachable.ql
@@ -0,0 +1,21 @@
+/**
+ * New-CFG version of NoSharedReachable.
+ *
+ * Original:
+ * Checks that two annotations sharing a timestamp value are on
+ * mutually exclusive CFG paths (neither can reach the other).
+ */
+
+import python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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/NewCfgStrictForward.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgStrictForward.expected
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgStrictForward.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgStrictForward.ql
new file mode 100644
index 000000000000..ebbc60346db0
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NewCfgStrictForward.ql
@@ -0,0 +1,22 @@
+/**
+ * New-CFG version of StrictForward.
+ *
+ * Original:
+ * 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 python
+import TimerUtils
+import NewCfgImpl
+
+private module Utils = EvalOrderCfgUtils<NewCfg>;
+
+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
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..e69de29bb2d1
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..4acf45db3cda
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql
@@ -0,0 +1,19 @@
+/**
+ * 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 python
+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..5568bd2a9a4a
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBasicBlock.ql
@@ -0,0 +1,16 @@
+/**
+ * Checks that every annotated CFG node belongs to a basic block.
+ */
+
+import python
+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..1fcceb2aca98
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql
@@ -0,0 +1,18 @@
+/**
+ * Checks that two annotations sharing a timestamp value are on
+ * mutually exclusive CFG paths (neither can reach the other).
+ */
+
+import python
+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/OldCfgImpl.qll b/python/ql/test/library-tests/ControlFlow/evaluation-order/OldCfgImpl.qll
new file mode 100644
index 000000000000..6ddfe672de75
--- /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(Scope s) { result = s.getEntryNode() }
+}
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..e69de29bb2d1
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..9e64770bab4d
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql
@@ -0,0 +1,19 @@
+/**
+ * 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 python
+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
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..dc46f00f6f56
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/TimerUtils.qll
@@ -0,0 +1,525 @@
+/**
+ * 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.
+ */
+
+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()
+}
+
+/** A timer annotation in the AST. */
+private newtype TTimerAnnotation =
+  /** `expr @ t[n]` or `expr @ t[n, m, ...]` */
+  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)
+    )
+  } or
+  /** `expr @ t.dead[n]` — dead-code annotation */
+  TDeadAnnotation(TestFunction func, Expr annotated, Expr timestamps) {
+    exists(BinaryExpr be |
+      be.getOp() instanceof MatMult and
+      be.getRight().(Subscript).getObject().(Attribute).getObject("dead").(Name).getId() =
+        func.getTimerParamName() and
+      be.getScope().getEnclosingScope*() = func and
+      annotated = be.getLeft() and
+      timestamps = be.getRight().(Subscript).getIndex()
+    )
+  } or
+  /** `expr @ t.never` — annotation for code that should never be evaluated */
+  TNeverAnnotation(TestFunction func, Expr annotated) {
+    exists(BinaryExpr be |
+      be.getOp() instanceof MatMult and
+      be.getRight().(Attribute).getObject("never").(Name).getId() = func.getTimerParamName() and
+      be.getScope().getEnclosingScope*() = func and
+      annotated = be.getLeft()
+    )
+  }
+
+/** A timer annotation (wrapping the newtype for a clean API). */
+class TimerAnnotation extends TTimerAnnotation {
+  /** Gets a timestamp value from this annotation. */
+  int getATimestamp() { exists(this.getTimestampExpr(result)) }
+
+  /** Gets the source expression for timestamp value `ts`. */
+  IntegerLiteral getTimestampExpr(int ts) {
+    result = timestampLiteral(this.getTimestampsExpr()) and
+    result.getValue() = ts
+  }
+
+  /** Gets the raw timestamp expression (single int 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 this is a dead-code annotation (`t.dead[n]`). */
+  predicate isDead() { this instanceof DeadTimerAnnotation }
+
+  /** Holds if this is a never-evaluated annotation (`t.never`). */
+  predicate isNever() { this instanceof NeverTimerAnnotation }
+
+  string toString() { result = this.getAnnotatedExpr().toString() }
+
+  Location getLocation() { result = this.getAnnotatedExpr().getLocation() }
+}
+
+/** A matmul-based timer annotation: `expr @ t[n]`. */
+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 }
+}
+
+/** A dead-code timer annotation: `expr @ t.dead[n]`. */
+class DeadTimerAnnotation extends TDeadAnnotation, TimerAnnotation {
+  TestFunction func;
+  Expr annotated;
+  Expr timestamps;
+
+  DeadTimerAnnotation() { this = TDeadAnnotation(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 never-evaluated annotation: `expr @ t.never`. */
+class NeverTimerAnnotation extends TNeverAnnotation, TimerAnnotation {
+  TestFunction func;
+  Expr annotated;
+
+  NeverTimerAnnotation() { this = TNeverAnnotation(func, annotated) }
+
+  override Expr getTimestampsExpr() { none() }
+
+  override TestFunction getTestFunction() { result = func }
+
+  override Expr getAnnotatedExpr() { result = annotated }
+
+  override BinaryExpr getTimerExpr() { result.getLeft() = 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 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 this is a dead-code annotation. */
+    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)
+    )
+  }
+
+  /** 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(NeverTimerAnnotation ann) {
+      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 `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..9958d922ec8f
--- /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
+
+
+@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..f2ece3a0820d
--- /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
+
+
+@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..d8183cb64842
--- /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
+
+
+@test
+def test_and_both_sides(t):
+    # True and X — both operands evaluated, result is X
+    x = (True @ t[0] and 42 @ t[1]) @ t[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]
+
+
+@test
+def test_or_short_circuit(t):
+    # True or ... — right side never evaluated
+    x = (True @ t[0] or False @ t.dead[1]) @ t[1]
+
+
+@test
+def test_or_both_sides(t):
+    # False or X — both operands evaluated, result is X
+    x = (False @ t[0] or 42 @ t[1]) @ t[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] and 3 @ t[2]) @ t[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] or 42 @ t[2]) @ t[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]) @ t[2] or 42 @ t[3]) @ t[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..2c543e913e4d
--- /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
+
+
+@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..3190e94c6eba
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/test_if.py
@@ -0,0 +1,108 @@
+"""If/elif/else control flow evaluation order."""
+
+from timer import test
+
+
+@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]
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..e81c31acde5c
--- /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
+
+
+# 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] + j @ t[7, 10, 16, 19]) @ t[8, 11, 17, 20]
+    done = True @ t[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..1dac5b0985c9
--- /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
+
+
+@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..d54730478b11
--- /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
+
+
+# 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..6cec3fd50cba
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/timer.py
@@ -0,0 +1,185 @@
+"""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
+
+    @test
+    def test_sequential(t):
+        x = 1 @ t[0]
+        y = 2 @ t[1]
+        z = (x + y) @ t[2]
+
+Usage with context manager (manual):
+
+    from timer import Timer
+
+    with Timer("my_test") as t:
+        x = 1 @ t[0]
+
+Timer API:
+    t[n]          - assert current timestamp is n, return marker
+    t[n, m, ...]  - assert current timestamp is one of {n, m, ...}
+    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."""
+
+    __slots__ = ("_timer", "_expected")
+
+    def __init__(self, timer, expected):
+        self._timer = timer
+        self._expected = expected
+
+    def __rmatmul__(self, value):
+        ts = self._timer._tick()
+        if ts not in self._expected:
+            self._timer._error(
+                f"expected {sorted(self._expected)}, 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 _NeverCheck:
+    """Marker returned by t.never — fails if the expression is ever evaluated."""
+
+    def __init__(self, timer):
+        self._timer = timer
+
+    def __rmatmul__(self, value):
+        self._timer._error("expression annotated with t.never was evaluated")
+        return value
+
+
+class _DeadCheck:
+    """Marker returned by t.dead[n] — fails if the expression is ever evaluated."""
+
+    def __init__(self, timer):
+        self._timer = timer
+
+    def __rmatmul__(self, value):
+        self._timer._error("expression annotated with t.dead was evaluated")
+        return value
+
+
+class _DeadSubscript:
+    """Subscriptable returned by t.dead — produces _DeadCheck markers."""
+
+    def __init__(self, timer):
+        self._timer = timer
+
+    def __getitem__(self, key):
+        return _DeadCheck(self._timer)
+
+
+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 = {}
+        self.dead = _DeadSubscript(self)
+        self.never = _NeverCheck(self)
+
+    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, list(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)