Author: mramalho Date: Sat Jun 16 07:36:17 2018 New Revision: 334891 URL: http://llvm.org/viewvc/llvm-project?rev=334891&view=rev Log: [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 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=334891&r1=334890&r2=334891&view=diff ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Sat Jun 16 07:36:17 2018 @@ -35,6 +35,8 @@ public: /// Checks if the added constraints are satisfiable virtual clang::ento::ConditionTruthVal isModelFeasible() = 0; + /// Dumps SMT formula + LLVM_DUMP_METHOD virtual void dump() const = 0; }; // end class SMTConstraintManager } // namespace ento Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=334891&r1=334890&r2=334891&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Sat Jun 16 07:36:17 2018 @@ -911,6 +911,8 @@ public: ConditionTruthVal isModelFeasible() override; + LLVM_DUMP_METHOD void dump() const override; + //===------------------------------------------------------------------===// // Implementation for interface from ConstraintManager. //===------------------------------------------------------------------===// @@ -1299,6 +1301,11 @@ clang::ento::ConditionTruthVal Z3Constra return ConditionTruthVal(); } +LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const +{ + Solver.dump(); +} + //===------------------------------------------------------------------===// // Internal implementation. //===------------------------------------------------------------------===// _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
