r334891 - [analyzer] Add method to the generic SMT API to dump the SMT formula

[Mikhail R. Gadelha via cfe-commits]

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.
 //===------------------------------------------------------------------===//