summaryrefslogtreecommitdiffstats
path: root/llvm/tools/llvm-readobj/llvm-readobj.h
diff options
context:
space:
mode:
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>2018-06-04 14:40:44 +0000
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>2018-06-04 14:40:44 +0000
commit8cd2ee1f2446aa6b0164befafcb990d2a637f464 (patch)
tree90695dacda2aed92d6fb5364ab3bfcc5b404dbd2 /llvm/tools/llvm-readobj/llvm-readobj.h
parent771e3beea6757d04ecbe7ed3a0df19af211d3d22 (diff)
downloadbcm5719-llvm-8cd2ee1f2446aa6b0164befafcb990d2a637f464.tar.gz
bcm5719-llvm-8cd2ee1f2446aa6b0164befafcb990d2a637f464.zip
[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 'llvm/tools/llvm-readobj/llvm-readobj.h')
0 files changed, 0 insertions, 0 deletions
OpenPOWER on IntegriCloud