[PATCH] D49074: [Analyzer] [WIP] Basic support for multiplication and division in the constraint manager

George Karpenkov via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Tue Aug 14 12:04:26 PDT 2018


george.karpenkov added a comment.

@baloghadamsoftware @xazax.hun we've had very promising results with using Z3 for refutation so far, almost at no cost, see Mikhail's recent email on cfe-dev (and sometimes at a negative cost!).
Do you still not want to try it first? False negatives could be addressed as well separately (e.g. by giving a checkers an option to cross-check the report with a more expensive solver before throwing), currently false positives are a far more pressing problem.


https://reviews.llvm.org/D49074





More information about the cfe-commits mailing list