NoQ added a comment.

The unconstrained rearrangements for `+`/`-`/`==`/`!=` are definitely good to 
go regardless of anything else.

Within the checker, we propose to manually simplify both `$x - N < $x` and `$x 
+ N > $x` to true (where N is positive), because in general this is unsound 
(due to potential overflows), but for iterator position symbols this is **the** 
intended behavior (if `container.end() + N` overflows, it's even worse than a 
regular past-end access).

For the rest of the cases (`>`/`<` with mixed symbols), we propose to delay the 
decision for now. For now simply admit that the solver is not awesome. If we 
had a perfect solver, we wouldn't have to rearrange anything, so the root cause 
of the problem is in the solver, and we shouldn't be fixing it on the checker 
side. If, before turning the checker on by default, we prove through evaluation 
that this shortcoming of the solver is indeed a bigger problem for this checker 
than for the rest of the analyzer, and is also the biggest problem with the 
checker, we can still come up with something (eg. the already-existing max/4 
approach). But let's delay this until we see how bad this part of the problem 
actually is.


https://reviews.llvm.org/D35109



_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to