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 | 8cd2ee1f2446aa6b0164befafcb990d2a637f464 (patch) | |
tree | 90695dacda2aed92d6fb5364ab3bfcc5b404dbd2 /clang/lib/Frontend/CompilerInvocation.cpp | |
parent | 771e3beea6757d04ecbe7ed3a0df19af211d3d22 (diff) | |
download | llvm-8cd2ee1f2446aa6b0164befafcb990d2a637f464.zip llvm-8cd2ee1f2446aa6b0164befafcb990d2a637f464.tar.gz llvm-8cd2ee1f2446aa6b0164befafcb990d2a637f464.tar.bz2 |
[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
llvm-svn: 333903
Diffstat (limited to 'clang/lib/Frontend/CompilerInvocation.cpp')
0 files changed, 0 insertions, 0 deletions