[PATCH] D45517: [analyzer] False positive refutation with Z3

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In https://reviews.llvm.org/D45517#1116770, @george.karpenkov wrote:

> > I am not not sure that I got the idea what are you suggesting here. If we have the constraint of for example a symbol s > 10 and later on a path we discover s > 20, will we also deduplicate this that way?
>
> No. But I thought in your optimization atoms inside the constraints would be the same?
>  Could you give an example where they are not?


So the logic in the current patch would be the following. When the symbol s dies it will be cleaned up from the state. For each symbol we will find the state where it was cleaned up. We will add the constraint for that symbol from the state before the cleanup which will contain the constraint `s > 20`. This is the only point where we add the constraints regarding the symbol `s`, so `s > 10` later on while we are traversing the path backwards will not be added.

Code to trigger this behavior:

  void f(int s) {
    if (s > 10) {
      // ...
      if (s > 20) {
          // trigger a warning
      }
    }
  }

So the point of this optimization is to only add the ranges of a symbol once, where we have the most information about it. So strictly speaking it is not a deduplication on the constraint level but on the symbol level.


https://reviews.llvm.org/D45517