[analyzer] Add method to the generic SMT API to dump the SMT formula
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Sat, 16 Jun 2018 14:36:17 +0000 (14:36 +0000)
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Sat, 16 Jun 2018 14:36:17 +0000 (14:36 +0000)
commite7f703804d7dadbd57cf7c50f479324d012f09e7
tree338143c0a1cb15d416b9e4c676ee25de710c5c53
parent1193bbf6b76b333069209f4f9224cb1f433f23ef
[analyzer] Add method to the generic SMT API to dump the SMT formula

Summary:
New method dump the SMT formula and the Z3 implementation.

There is no test because I only used it for debugging.

However, if requested, I can add an option to the static analyzer to dump the formula (whole program? per path?), maybe something like the trimmed graph but for SMT formulas.

Reviewers: NoQ, george.karpenkov, ddcc

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

Differential Revision: https://reviews.llvm.org/D48221

llvm-svn: 334891
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp