[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#1156609, @george.karpenkov wrote:

> The overall point is that writing this kind of code is *extremely* error-prone.


Every modifications on the core is extremely error-prone. That is why we must cross check it and only apply it if it is 100% mathematically correct. This patch is only WIP for now. Freezing the core in its current state helps us to not introduce new errors but also prevents improving the current functionality which is not yet sufficient for many of our customers. What I did is not hacking, multiplicative operations can be implemented a similar way to additive ones, they are just a bit more complex.

> We are actually considering going in a different direction and doing a rollback for the previous rearrangement patches due to some issues.

What issues could it cause since it is guarded by an option? As for the rearrangement of the additive operations it was @NoQ's idea but I agree there. Actually I feel this rearrangement patch a bit of hacking, but I also agree with @NoQ that it may be useful for other checkers as well. That was the reason to put it into `SValBuilder` instead of the checker itself. As you may be aware of it I originally did the rearrangement inside the checker.

> Could you see whether Z3 visitor would meet your needs?

We will look at it, but please read my previous answer.


https://reviews.llvm.org/D49074