Skip to content

Commit

Permalink
[analyzer] Use the macro REGISTER_TRAIT_WITH_PROGRAMSTATE in the Z3 b…
Browse files Browse the repository at this point in the history
…ackend

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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@337923 91177308-0d34-0410-b5e6-96231b3b80d8
  • Loading branch information
mikhailramalho committed Jul 25, 2018
1 parent 7179078 commit 18b6344
Showing 1 changed file with 7 additions and 22 deletions.
29 changes: 7 additions & 22 deletions lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -313,6 +291,13 @@ static bool areEquivalent(const llvm::fltSemantics &LHS,
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;

Expand Down

0 comments on commit 18b6344

Please sign in to comment.