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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D103440#2891915 <https://reviews.llvm.org/D103440#2891915>, @manas wrote:

> Here is the proof of correctness of the algorithm using Z3: https://gist.github.com/weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25

There is a couple of fundamental problems there that you need to resolve.  I left my comments there.



================
Comment at: clang/test/Analysis/constant-folding.c:260
+
+  // Overflows on both ends
+  if (a >= 5 && a <= UINT_MAX - 5 && b <= 10) {
----------------
This looks like an overflow on one end (we couldn't have them on both ends with addition and unsigned integers) and wrapping around surpassing the beginning of the range.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103440