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