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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
