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

[Balogh, Ádám via Phabricator via cfe-commits]

baloghadamsoftware added a comment.

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

> @baloghadamsoftware @dkrupp @xazax.hun Interesting. What do you think about instead using Z3 cross-check functionality recently added, to solve this and all other similar problems instead?


As far as I know the purpose of the cross-check functionality is to execute Z3 only on actual bug report paths. This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

As we discussed with @dcoughlin at the Euro LLVM 2018 the community should consider a new constraint manager, which is in between the range-based one and the Z3 both feature and performance wise. However, this is something long term, until then we should improve the existing one  as far as reasonable. I am sure that multiplicative operations can be solved similarly to the additive ones.


https://reviews.llvm.org/D49074