[PATCH] D49074: [Analyzer] [WIP] Basic support for multiplication and division in the constraint manager

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

xazax.hun added a comment.

In https://reviews.llvm.org/D49074#1159095, @george.karpenkov wrote:

> > This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.
>
> Do you have examples of those? In my understanding, (almost) all of the imprecisions in the solver lead purely to false positives.
>  The only example where you lose bugs is when you stop exploring due to reaching a (false) fatal error.


This is not an example from the iterator checker (hopefully Adam will provide us with one example from there) but think of division by zero. The division by zero check will only warn if a value is constrained to be zero. The imprecision in the built in solver might result in failure to constrain a value to zero while the Z3 might be able to do that.


https://reviews.llvm.org/D49074