Python: Add ConsecutiveTimestamps test

This one is potentially a bit iffy -- it checks for a very powerful
propetry (that implies many of the other queries), but as the test
results show, it can produce false positives when there is in fact no
problem. We may want to get rid of it entirely, if it becomes too noisy.

Author: tausbn

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 |

python/ql/test/library-tests/ControlFlow/evaluation-order/ConsecutiveTimestamps.ql

@@ -0,0 +1,46 @@
+/**
+ * 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
+
+/**
+ * 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.getExpr().getScope() != f
+  )
+}
+
+from TimerAnnotation ann, int a
+where
+  not hasNestedScopeAnnotation(ann.getTestFunction()) and
+  not ann.isDead() and
+  a = ann.getATimestamp() and
+  not exists(TimerCfgNode x, TimerCfgNode y |
+    ann.getExpr() = 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()
+    )
+select ann, "$@ in $@ has no consecutive successor (expected " + (a + 1) + ")",
+  ann.getTimestampExpr(a), "Timestamp " + a, ann.getTestFunction(), ann.getTestFunction().getName()