Merge pull request #10355 from MathiasVP/fix-unequalIntegralSsa-standard-order

C++: Avoid bad standard order in range analysis

Author: MathiasVP

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll

@@ -542,12 +542,32 @@ private predicate unequalIntegralSsa(
 ) {
   exists(SemExpr e, int d1, int d2 |
     unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
-    bounded(e, b, d2, true, _, _, _) and
-    bounded(e, b, d2, false, _, _, _) and
+    boundedUpper(e, b, d1) and
+    boundedLower(e, b, d2) and
     delta = d2 + d1
   )
 }
 
+/**
+ * Holds if `b + delta` is an upper bound for `e`.
+ *
+ * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
+ */
+pragma[nomagic]
+private predicate boundedUpper(SemExpr e, SemBound b, int delta) {
+  bounded(e, b, delta, true, _, _, _)
+}
+
+/**
+ * Holds if `b + delta` is a lower bound for `e`.
+ *
+ * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
+ */
+pragma[nomagic]
+private predicate boundedLower(SemExpr e, SemBound b, int delta) {
+  bounded(e, b, delta, false, _, _, _)
+}
+
 /** Weakens a delta to lie in the range `[-1..1]`. */
 bindingset[delta, upper]
 private int weakenDelta(boolean upper, int delta) {