[TODO]: Only partial solution to range analysis.

Author: michaelnebel

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll

@@ -33,7 +33,9 @@ private module Impl {
   /** Holds if SSA definition `def` equals `e + delta`. */
   predicate ssaUpdateStep(ExplicitDefinition def, ExprNode e, int delta) {
     exists(ControlFlow::Node cfn | cfn = def.getControlFlowNode() |
-      e = cfn.(ExprNode::Assignment).getRValue() and delta = 0
+      e = cfn.(ExprNode::Assignment).getRValue() and
+      delta = 0 and
+      not cfn instanceof ExprNode::AssignOperation
       or
       e = cfn.(ExprNode::PostIncrExpr).getOperand() and delta = 1
       or
@@ -66,6 +68,12 @@ private module Impl {
       x.getIntValue() = delta
     )
     or
+    exists(ConstantIntegerExpr x |
+      e2.(ExprNode::AssignAddExpr).getLeftOperand() = e1 and
+      e2.(ExprNode::AssignAddExpr).getRightOperand() = x and
+      x.getIntValue() = delta
+    )
+    or
     exists(ConstantIntegerExpr x |
       e2.(ExprNode::SubExpr).getLeftOperand() = e1 and
       e2.(ExprNode::SubExpr).getRightOperand() = x and
@@ -230,6 +238,11 @@ module ExprNode {
     override CS::AssignExpr e;
   }
 
+  /** A compound assignment operation. */
+  class AssignOperation extends Assignment, BinaryOperation {
+    override CS::AssignOperation e;
+  }
+
   /** A unary operation. */
   class UnaryOperation extends ExprNode {
     override CS::UnaryOperation e;
@@ -327,6 +340,12 @@ module ExprNode {
     override TAddOp getOp() { any() }
   }
 
+  class AssignAddExpr extends AssignOperation {
+    override CS::AssignAddExpr e;
+
+    override TAddOp getOp() { any() }
+  }
+
   /** A subtraction operation. */
   class SubExpr extends BinaryOperation {
     override CS::SubExpr e;