[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

Hey, great start!
I added my comments inline and other mentors as reviewers.



================
Comment at: clang/test/Analysis/constant-folding.c:275
+
+    if (a <= UINT_MAX && b <= UINT_MAX) {
+      clang_analyzer_eval((a + b) < 0); // expected-warning{{UNKNOWN}}
----------------
I think this is always true.


================
Comment at: clang/test/Analysis/constant-folding.c:287
+  if (c < 0 && d < 0) {
+    clang_analyzer_eval((c + d) == 0); // expected-warning{{TRUE}}
+
----------------
I'm not sure I understand why do you make this assumption.


================
Comment at: clang/test/Analysis/constant-folding.c:290-291
+    if (c > INT_MIN) {
+      clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
+      clang_analyzer_eval((c + d) == INT_MAX<<1); // expected-warning{{TRUE}}
+    }
----------------
Here is the same note, `clang_analyzer_eval` doesn't produce `TRUE` only because this condition might be true.


================
Comment at: clang/test/Analysis/constant-folding.c:298
+    clang_analyzer_eval((c + d) != 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval((c + d) < 0); // expected-warning{{TRUE}}
+  }
----------------
If `c == d == 1` this doesn't hold. Did you want to check here that we account for overflows?


================
Comment at: clang/test/Analysis/constant-folding.c:302
+  // Checks for inclusive ranges
+  if (a >= 0 && a <= 10 && b >= -20 && b <= 20) {
+    clang_analyzer_eval((a + b) >= -20); // expected-warning{{TRUE}}
----------------
What about other cases here? I mean specifically when two ranges are have a form `[A, B]`


================
Comment at: clang/test/Analysis/constant-folding.c:305
+    clang_analyzer_eval((a + b) <= 30); // expected-warning{{TRUE}}
+    clang_analyzer_eval((a + b) == -20); // expected-warning{{TRUE}}
+  }
----------------
`clang_analyzer_eval` returns `TRUE` only if we can deduct that this expression on a particular path is **always** true.  Here it's not going to hold.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103440/new/

https://reviews.llvm.org/D103440