NoQ added a comment. In https://reviews.llvm.org/D35110#1117401, @baloghadamsoftware wrote:
> Sorry, Artem, but it does not work this way. Even if the symbolic expressions > are constrained to `[-MAX/4..MAX/4]`, after rearrangement the difference > still uses the whole range, thus `m>n` becomes `m-n>0`, where in the false > branch the range for `m-n` is `[MIN..0]`. Then if we check `n>=m` the range > set is reversed to `[MIN..MIN]U[0..MAX]` which results `UNKNOWN` for `n-m`. > It does not solve any of our problems and there is no remedy on the checker's > side. Which expressions are constrained? Why does the difference use the whole range? Is it something that could have been fixed by the "enforce that separately" part in my old comment: > iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], > right? So if we subtract one such symbol from another, it's going to be in > range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the > iterator checker to enforce that separately? ? https://reviews.llvm.org/D35110 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
