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.
cfe-commits mailing list