baloghadamsoftware added a comment. In https://reviews.llvm.org/D35110#972430, @NoQ wrote:
> In https://reviews.llvm.org/D35110#969782, @baloghadamsoftware wrote: > > > Strange, but modifying the tests from `m <relation> n` to `m - n <relation> > > 0` does not help. The statement `if (m - n <relation> 0)` does not store a > > range for `m - n` in the constraint manager. With the other patch which > > automatically changes `m <relation> n` to `m - n <relation> 0` the range is > > stored automatically. > > > I guess we can easily assume how a `SymIntExpr` relates to a number by > storing a range on the opaque left-hand-side symbol, no matter how > complicated it is, but we cannot assume how a symbol relates to a symbol > (there's no obvious range to store). That's just how `assumeSym` currently > works. Actually it happens because `m - n` evaluates to `Unknown`. The code part responsible for this is the beginning of `SValBuilder::makeSymExprValNN()`, which prevents `m - n`-like symbolic expression unless one of `m` or `n` is `Tainted`. Anna added this part 5-6 years ago because some kind of bug, but it seems that it still exists. If I try to remove it then one test executes for days (with loop max count 63 or 64) and two tests fail with an assert. https://reviews.llvm.org/D35110 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
