r337923 - [analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 25 05:49:47 PDT 2018
Author: mramalho
Date: Wed Jul 25 05:49:47 2018
New Revision: 337923
URL: http://llvm.org/viewvc/llvm-project?rev=337923&view=rev
Log:
[analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 backend
Summary:
The macro was manually expanded in the Z3 backend and this patch adds it back.
Adding the expanded code is dangerous as the macro may change in the future and the expanded code might be left outdated.
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D49769
Modified:
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337923&r1=337922&r2=337923&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:47 2018
@@ -25,28 +25,6 @@ using namespace ento;
#include <z3.h>
-// Forward declarations
-namespace {
-class Z3Expr;
-class ConstraintZ3 {};
-} // end anonymous namespace
-
-typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
-
-// Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair)
-namespace clang {
-namespace ento {
-template <>
-struct ProgramStateTrait<ConstraintZ3>
- : public ProgramStatePartialTrait<ConstraintZ3Ty> {
- static void *GDMIndex() {
- static int Index;
- return &Index;
- }
-};
-} // end namespace ento
-} // end namespace clang
-
namespace {
class Z3Config {
@@ -313,6 +291,13 @@ static bool areEquivalent(const llvm::fl
llvm::APFloat::semanticsSizeInBits(RHS));
}
+} // end anonymous namespace
+
+typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
+REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty)
+
+namespace {
+
class Z3Solver : public SMTSolver {
friend class Z3ConstraintManager;
More information about the cfe-commits
mailing list