summaryrefslogtreecommitdiffstats
path: root/clang/test/Analysis/z3-crosscheck.c
Commit message (Collapse)AuthorAgeFilesLines
* [analyzer] fix test case expected warningMikhail R. Gadelha2018-06-281-8/+0
| | | | | | | | | After r335814, the constraint manager is no longer generating a false bug report about the division by zero in the test case. This patch removes the expected false bug report. llvm-svn: 335932
* [analyzer] False positive refutation with Z3Mikhail R. Gadelha2018-06-041-0/+51
Summary: This is a prototype of a bug reporter visitor that invalidates bug reports by re-checking constraints of certain states on the bug path using the Z3 constraint manager backend. The functionality is available under the `crosscheck-with-z3` analyzer config flag. Reviewers: george.karpenkov, NoQ, dcoughlin, rnkovacs Reviewed By: george.karpenkov Subscribers: rnkovacs, NoQ, george.karpenkov, dcoughlin, xbolva00, ddcc, mikhail.ramalho, MTC, fhahn, whisperity, baloghadamsoftware, szepet, a.sidorin, gsd, dkrupp, xazax.hun, cfe-commits Differential Revision: https://reviews.llvm.org/D45517 llvm-svn: 333903
OpenPOWER on IntegriCloud