[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

Gabor Marton via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Fri Oct 15 06:50:11 PDT 2021


martong added a comment.

After taking a look at the new findings we discovered, there is a logic error with this patch, actually `a % b == 0 implies that a == 0` does not hold, one counter example is `10 % 2 == 0`. Argh, probably we should be using Z3 next time to prove or disprove such things. Or perhaps other reviewers with strong math background could have had a look (knock knock @NoQ :).


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D110357/new/

https://reviews.llvm.org/D110357



More information about the cfe-commits mailing list