diff options
| author | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-06-04 14:40:44 +0000 |
|---|---|---|
| committer | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-06-04 14:40:44 +0000 |
| commit | 9f72894e31a3b8c5042f221ace91727a81391d80 (patch) | |
| tree | dba8308e08b58c502cb49110a9dce540f7512bd8 /lib/Frontend/CompilerInvocation.cpp | |
| parent | 9aed45542a597d01c4dcd48ced335ba28bb6063d (diff) | |
| download | clang-9f72894e31a3b8c5042f221ace91727a81391d80.tar.gz | |
[analyzer] False positive refutation with Z3
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
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@333903 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Frontend/CompilerInvocation.cpp')
0 files changed, 0 insertions, 0 deletions