This revision was automatically updated to reflect the committed changes.
Closed by commit rL334891: [analyzer] Add method to the generic SMT API to dump
the SMT formula (authored by mramalho, committed by ).
Herald added a subscriber: llvm-commits.
Changed prior to commit:
https://reviews.llvm.org/D48221?vs=151531&id=151618#toc
Repository:
rL LLVM
https://reviews.llvm.org/D48221
Files:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Index:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
---
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -35,6 +35,8 @@
/// 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
Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -911,6 +911,8 @@
ConditionTruthVal isModelFeasible() override;
+ LLVM_DUMP_METHOD void dump() const override;
+
//===------------------------------------------------------------------===//
// Implementation for interface from ConstraintManager.
//===------------------------------------------------------------------===//
@@ -1299,6 +1301,11 @@
return ConditionTruthVal();
}
+LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const
+{
+ Solver.dump();
+}
+
//===------------------------------------------------------------------===//
// Internal implementation.
//===------------------------------------------------------------------===//
Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -35,6 +35,8 @@
/// 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
Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -911,6 +911,8 @@
ConditionTruthVal isModelFeasible() override;
+ LLVM_DUMP_METHOD void dump() const override;
+
//===------------------------------------------------------------------===//
// Implementation for interface from ConstraintManager.
//===------------------------------------------------------------------===//
@@ -1299,6 +1301,11 @@
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
