[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