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

[Manas Gupta via Phabricator via cfe-commits]

manas added a comment.

@NoQ I figured out the tests but while testing against Z3, I mixed up constraints. I am changing those.



================
Comment at: clang/test/Analysis/constant-folding.c:265
+    if (a > INT_MAX) {
+      clang_analyzer_eval((a + b) <= 0); // expected-warning{{FALSE}}
+      clang_analyzer_eval((a + b) > 0); // expected-warning{{FALSE}}
----------------
xazax.hun wrote:
> Since both `a` and `b` are unsigned values, their sum is also unsigned. We basically check if their sum could be zero. I don't see why it could not in this case (e.g. when `b == UINT_MAX - a + 1`). Do I miss something?
I am editing that condition to be `b >= INT_MAX`.


================
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}}
----------------
xazax.hun wrote:
> vsavchenko wrote:
> > I think this is always true.
> So is `a >= 0 && b >= 0` unless I miss something.
@vsavchenko true, I am removing that conditional as it serves no purpose there.

@xazax.hun that's true.


================
Comment at: clang/test/Analysis/constant-folding.c:282
+  if (a == UINT_MAX && b == UINT_MAX) {
+    clang_analyzer_eval((a + b) >= 0); // expected-warning{{FALSE}}
+  }
----------------
xazax.hun wrote:
> I think `UINT_MAX + UINT_MAX` supposed to be positive. Do I miss something here?
Should not `UINT_MAX + UINT_MAX` wrap around to be negative? I think I misunderstood it.


================
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}}
+    }
----------------
vsavchenko wrote:
> Here is the same note, `clang_analyzer_eval` doesn't produce `TRUE` only because this condition might be true.
understood.


================
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}}
+  }
----------------
vsavchenko wrote:
> If `c == d == 1` this doesn't hold. Did you want to check here that we account for overflows?
Yes, I was checking for that. I am changing that case.


================
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}}
----------------
vsavchenko wrote:
> What about other cases here? I mean specifically when two ranges are have a form `[A, B]`
I am adding more cases here.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103440