forked from OSchip/llvm-project
[analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.
Summary: By making SMTConstraintManager a template and passing the SMT constraint type and expr, we can further move code from the Z3ConstraintManager class to the generic SMT constraint Manager. Now, each SMT specific constraint manager only needs to implement the method `bool canReasonAbout(SVal X) const`. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: mgorny, xazax.hun, szepet, a.sidorin, Szelethus Differential Revision: https://reviews.llvm.org/D50770 llvm-svn: 340533
This commit is contained in:
Mikhail R. Gadelha
parent
2420ee9b91
commit
b0670d349c
|
|
@ -21,6 +21,7 @@
|
|||
namespace clang {
|
||||
namespace ento {
|
||||
|
||||
template <typename ConstraintSMT, typename SMTExprTy>
|
||||
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
|
||||
SMTSolverRef &Solver;
|
||||
|
||||
|
|
@ -34,25 +35,191 @@ public:
|
|||
// Implementation for interface from SimpleConstraintManager.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
|
||||
bool Assumption) override;
|
||||
ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
|
||||
bool Assumption) override {
|
||||
ASTContext &Ctx = getBasicVals().getContext();
|
||||
|
||||
QualType RetTy;
|
||||
bool hasComparison;
|
||||
|
||||
SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
|
||||
|
||||
// Create zero comparison for implicit boolean cast, with reversed
|
||||
// assumption
|
||||
if (!hasComparison && !RetTy->isBooleanType())
|
||||
return assumeExpr(State, Sym,
|
||||
Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
|
||||
|
||||
return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
|
||||
}
|
||||
|
||||
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
|
||||
const llvm::APSInt &From,
|
||||
const llvm::APSInt &To,
|
||||
bool InRange) override;
|
||||
bool InRange) override {
|
||||
ASTContext &Ctx = getBasicVals().getContext();
|
||||
return assumeExpr(State, Sym,
|
||||
Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
|
||||
}
|
||||
|
||||
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
|
||||
bool Assumption) override;
|
||||
bool Assumption) override {
|
||||
// Skip anything that is unsupported
|
||||
return State;
|
||||
}
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Implementation for interface from ConstraintManager.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
|
||||
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
|
||||
ASTContext &Ctx = getBasicVals().getContext();
|
||||
|
||||
QualType RetTy;
|
||||
// The expression may be casted, so we cannot call getZ3DataExpr() directly
|
||||
SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
|
||||
SMTExprRef Exp =
|
||||
Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
|
||||
|
||||
// Negate the constraint
|
||||
SMTExprRef NotExp =
|
||||
Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
|
||||
|
||||
Solver->reset();
|
||||
addStateConstraints(State);
|
||||
|
||||
Solver->push();
|
||||
Solver->addConstraint(Exp);
|
||||
ConditionTruthVal isSat = Solver->check();
|
||||
|
||||
Solver->pop();
|
||||
Solver->addConstraint(NotExp);
|
||||
ConditionTruthVal isNotSat = Solver->check();
|
||||
|
||||
// Zero is the only possible solution
|
||||
if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
|
||||
return true;
|
||||
|
||||
// Zero is not a solution
|
||||
if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
|
||||
return false;
|
||||
|
||||
// Zero may be a solution
|
||||
return ConditionTruthVal();
|
||||
}
|
||||
|
||||
const llvm::APSInt *getSymVal(ProgramStateRef State,
|
||||
SymbolRef Sym) const override;
|
||||
SymbolRef Sym) const override {
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
ASTContext &Ctx = BVF.getContext();
|
||||
|
||||
if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
|
||||
QualType Ty = Sym->getType();
|
||||
assert(!Ty->isRealFloatingType());
|
||||
llvm::APSInt Value(Ctx.getTypeSize(Ty),
|
||||
!Ty->isSignedIntegerOrEnumerationType());
|
||||
|
||||
SMTExprRef Exp =
|
||||
Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
|
||||
|
||||
Solver->reset();
|
||||
addStateConstraints(State);
|
||||
|
||||
// Constraints are unsatisfiable
|
||||
ConditionTruthVal isSat = Solver->check();
|
||||
if (!isSat.isConstrainedTrue())
|
||||
return nullptr;
|
||||
|
||||
// Model does not assign interpretation
|
||||
if (!Solver->getInterpretation(Exp, Value))
|
||||
return nullptr;
|
||||
|
||||
// A value has been obtained, check if it is the only value
|
||||
SMTExprRef NotExp = Solver->fromBinOp(
|
||||
Exp, BO_NE,
|
||||
Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
|
||||
: Solver->fromAPSInt(Value),
|
||||
false);
|
||||
|
||||
Solver->addConstraint(NotExp);
|
||||
|
||||
ConditionTruthVal isNotSat = Solver->check();
|
||||
if (isNotSat.isConstrainedTrue())
|
||||
return nullptr;
|
||||
|
||||
// This is the only solution, store it
|
||||
return &BVF.getValue(Value);
|
||||
}
|
||||
|
||||
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
|
||||
SymbolRef CastSym = SC->getOperand();
|
||||
QualType CastTy = SC->getType();
|
||||
// Skip the void type
|
||||
if (CastTy->isVoidType())
|
||||
return nullptr;
|
||||
|
||||
const llvm::APSInt *Value;
|
||||
if (!(Value = getSymVal(State, CastSym)))
|
||||
return nullptr;
|
||||
return &BVF.Convert(SC->getType(), *Value);
|
||||
}
|
||||
|
||||
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
|
||||
const llvm::APSInt *LHS, *RHS;
|
||||
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
|
||||
LHS = getSymVal(State, SIE->getLHS());
|
||||
RHS = &SIE->getRHS();
|
||||
} else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
|
||||
LHS = &ISE->getLHS();
|
||||
RHS = getSymVal(State, ISE->getRHS());
|
||||
} else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
|
||||
// Early termination to avoid expensive call
|
||||
LHS = getSymVal(State, SSM->getLHS());
|
||||
RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
|
||||
} else {
|
||||
llvm_unreachable("Unsupported binary expression to get symbol value!");
|
||||
}
|
||||
|
||||
if (!LHS || !RHS)
|
||||
return nullptr;
|
||||
|
||||
llvm::APSInt ConvertedLHS, ConvertedRHS;
|
||||
QualType LTy, RTy;
|
||||
std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
|
||||
std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
|
||||
Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
|
||||
Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
|
||||
return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
|
||||
}
|
||||
|
||||
llvm_unreachable("Unsupported expression to get symbol value!");
|
||||
}
|
||||
|
||||
ProgramStateRef removeDeadBindings(ProgramStateRef State,
|
||||
SymbolReaper &SymReaper) override {
|
||||
auto CZ = State->get<ConstraintSMT>();
|
||||
auto &CZFactory = State->get_context<ConstraintSMT>();
|
||||
|
||||
for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
|
||||
if (SymReaper.maybeDead(I->first))
|
||||
CZ = CZFactory.remove(CZ, *I);
|
||||
}
|
||||
|
||||
return State->set<ConstraintSMT>(CZ);
|
||||
}
|
||||
|
||||
void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
|
||||
const char *sep) override {
|
||||
|
||||
auto CZ = St->get<ConstraintSMT>();
|
||||
|
||||
OS << nl << sep << "Constraints:";
|
||||
for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
|
||||
OS << nl << ' ' << I->first << " : ";
|
||||
I->second.print(OS);
|
||||
}
|
||||
OS << nl;
|
||||
}
|
||||
|
||||
/// Dumps SMT formula
|
||||
LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
|
||||
|
|
@ -60,15 +227,44 @@ public:
|
|||
protected:
|
||||
// Check whether a new model is satisfiable, and update the program state.
|
||||
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
|
||||
const SMTExprRef &Exp) = 0;
|
||||
const SMTExprRef &Exp) {
|
||||
// Check the model, avoid simplifying AST to save time
|
||||
if (checkModel(State, Exp).isConstrainedTrue())
|
||||
return State->add<ConstraintSMT>(
|
||||
std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
|
||||
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
/// Given a program state, construct the logical conjunction and add it to
|
||||
/// the solver
|
||||
virtual void addStateConstraints(ProgramStateRef State) const = 0;
|
||||
virtual void addStateConstraints(ProgramStateRef State) const {
|
||||
// TODO: Don't add all the constraints, only the relevant ones
|
||||
auto CZ = State->get<ConstraintSMT>();
|
||||
auto I = CZ.begin(), IE = CZ.end();
|
||||
|
||||
// Construct the logical AND of all the constraints
|
||||
if (I != IE) {
|
||||
std::vector<SMTExprRef> ASTs;
|
||||
|
||||
SMTExprRef Constraint = Solver->newExprRef(I++->second);
|
||||
while (I != IE) {
|
||||
Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
|
||||
}
|
||||
|
||||
Solver->addConstraint(Constraint);
|
||||
}
|
||||
}
|
||||
|
||||
// Generate and check a Z3 model, using the given constraint.
|
||||
ConditionTruthVal checkModel(ProgramStateRef State,
|
||||
const SMTExprRef &Exp) const;
|
||||
const SMTExprRef &Exp) const {
|
||||
Solver->reset();
|
||||
Solver->addConstraint(Exp);
|
||||
addStateConstraints(State);
|
||||
return Solver->check();
|
||||
}
|
||||
|
||||
}; // end class SMTConstraintManager
|
||||
|
||||
} // namespace ento
|
||||
|
|
|
|||
|
|
@ -49,7 +49,6 @@ add_clang_library(clangStaticAnalyzerCore
|
|||
SVals.cpp
|
||||
SimpleConstraintManager.cpp
|
||||
SimpleSValBuilder.cpp
|
||||
SMTConstraintManager.cpp
|
||||
Store.cpp
|
||||
SubEngine.cpp
|
||||
SymbolManager.cpp
|
||||
|
|
|
|||
|
|
@ -1,181 +0,0 @@
|
|||
//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==//
|
||||
//
|
||||
// The LLVM Compiler Infrastructure
|
||||
//
|
||||
// This file is distributed under the University of Illinois Open Source
|
||||
// License. See LICENSE.TXT for details.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
|
||||
#include "clang/Basic/TargetInfo.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
|
||||
|
||||
using namespace clang;
|
||||
using namespace ento;
|
||||
|
||||
ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
|
||||
SymbolRef Sym,
|
||||
bool Assumption) {
|
||||
ASTContext &Ctx = getBasicVals().getContext();
|
||||
|
||||
QualType RetTy;
|
||||
bool hasComparison;
|
||||
|
||||
SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
|
||||
|
||||
// Create zero comparison for implicit boolean cast, with reversed assumption
|
||||
if (!hasComparison && !RetTy->isBooleanType())
|
||||
return assumeExpr(State, Sym,
|
||||
Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
|
||||
|
||||
return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
|
||||
}
|
||||
|
||||
ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, bool InRange) {
|
||||
ASTContext &Ctx = getBasicVals().getContext();
|
||||
return assumeExpr(State, Sym,
|
||||
Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
|
||||
}
|
||||
|
||||
ProgramStateRef
|
||||
SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
|
||||
bool Assumption) {
|
||||
// Skip anything that is unsupported
|
||||
return State;
|
||||
}
|
||||
|
||||
ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
|
||||
SymbolRef Sym) {
|
||||
ASTContext &Ctx = getBasicVals().getContext();
|
||||
|
||||
QualType RetTy;
|
||||
// The expression may be casted, so we cannot call getZ3DataExpr() directly
|
||||
SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
|
||||
SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
|
||||
|
||||
// Negate the constraint
|
||||
SMTExprRef NotExp =
|
||||
Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
|
||||
|
||||
Solver->reset();
|
||||
addStateConstraints(State);
|
||||
|
||||
Solver->push();
|
||||
Solver->addConstraint(Exp);
|
||||
ConditionTruthVal isSat = Solver->check();
|
||||
|
||||
Solver->pop();
|
||||
Solver->addConstraint(NotExp);
|
||||
ConditionTruthVal isNotSat = Solver->check();
|
||||
|
||||
// Zero is the only possible solution
|
||||
if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
|
||||
return true;
|
||||
|
||||
// Zero is not a solution
|
||||
if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
|
||||
return false;
|
||||
|
||||
// Zero may be a solution
|
||||
return ConditionTruthVal();
|
||||
}
|
||||
|
||||
const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
|
||||
SymbolRef Sym) const {
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
ASTContext &Ctx = BVF.getContext();
|
||||
|
||||
if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
|
||||
QualType Ty = Sym->getType();
|
||||
assert(!Ty->isRealFloatingType());
|
||||
llvm::APSInt Value(Ctx.getTypeSize(Ty),
|
||||
!Ty->isSignedIntegerOrEnumerationType());
|
||||
|
||||
SMTExprRef Exp =
|
||||
Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
|
||||
|
||||
Solver->reset();
|
||||
addStateConstraints(State);
|
||||
|
||||
// Constraints are unsatisfiable
|
||||
ConditionTruthVal isSat = Solver->check();
|
||||
if (!isSat.isConstrainedTrue())
|
||||
return nullptr;
|
||||
|
||||
// Model does not assign interpretation
|
||||
if (!Solver->getInterpretation(Exp, Value))
|
||||
return nullptr;
|
||||
|
||||
// A value has been obtained, check if it is the only value
|
||||
SMTExprRef NotExp = Solver->fromBinOp(
|
||||
Exp, BO_NE,
|
||||
Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
|
||||
: Solver->fromAPSInt(Value),
|
||||
false);
|
||||
|
||||
Solver->addConstraint(NotExp);
|
||||
|
||||
ConditionTruthVal isNotSat = Solver->check();
|
||||
if (isNotSat.isConstrainedTrue())
|
||||
return nullptr;
|
||||
|
||||
// This is the only solution, store it
|
||||
return &BVF.getValue(Value);
|
||||
}
|
||||
|
||||
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
|
||||
SymbolRef CastSym = SC->getOperand();
|
||||
QualType CastTy = SC->getType();
|
||||
// Skip the void type
|
||||
if (CastTy->isVoidType())
|
||||
return nullptr;
|
||||
|
||||
const llvm::APSInt *Value;
|
||||
if (!(Value = getSymVal(State, CastSym)))
|
||||
return nullptr;
|
||||
return &BVF.Convert(SC->getType(), *Value);
|
||||
}
|
||||
|
||||
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
|
||||
const llvm::APSInt *LHS, *RHS;
|
||||
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
|
||||
LHS = getSymVal(State, SIE->getLHS());
|
||||
RHS = &SIE->getRHS();
|
||||
} else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
|
||||
LHS = &ISE->getLHS();
|
||||
RHS = getSymVal(State, ISE->getRHS());
|
||||
} else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
|
||||
// Early termination to avoid expensive call
|
||||
LHS = getSymVal(State, SSM->getLHS());
|
||||
RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
|
||||
} else {
|
||||
llvm_unreachable("Unsupported binary expression to get symbol value!");
|
||||
}
|
||||
|
||||
if (!LHS || !RHS)
|
||||
return nullptr;
|
||||
|
||||
llvm::APSInt ConvertedLHS, ConvertedRHS;
|
||||
QualType LTy, RTy;
|
||||
std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
|
||||
std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
|
||||
Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
|
||||
Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
|
||||
return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
|
||||
}
|
||||
|
||||
llvm_unreachable("Unsupported expression to get symbol value!");
|
||||
}
|
||||
|
||||
ConditionTruthVal
|
||||
SMTConstraintManager::checkModel(ProgramStateRef State,
|
||||
const SMTExprRef &Exp) const {
|
||||
Solver->reset();
|
||||
Solver->addConstraint(Exp);
|
||||
addStateConstraints(State);
|
||||
return Solver->check();
|
||||
}
|
||||
|
|
@ -904,31 +904,13 @@ public:
|
|||
}
|
||||
}; // end class Z3Solver
|
||||
|
||||
class Z3ConstraintManager : public SMTConstraintManager {
|
||||
class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {
|
||||
SMTSolverRef Solver = CreateZ3Solver();
|
||||
|
||||
public:
|
||||
Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
|
||||
: SMTConstraintManager(SE, SB, Solver) {}
|
||||
|
||||
void addStateConstraints(ProgramStateRef State) const override {
|
||||
// TODO: Don't add all the constraints, only the relevant ones
|
||||
ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
|
||||
ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
|
||||
|
||||
// Construct the logical AND of all the constraints
|
||||
if (I != IE) {
|
||||
std::vector<SMTExprRef> ASTs;
|
||||
|
||||
SMTExprRef Constraint = Solver->newExprRef(I++->second);
|
||||
while (I != IE) {
|
||||
Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
|
||||
}
|
||||
|
||||
Solver->addConstraint(Constraint);
|
||||
}
|
||||
}
|
||||
|
||||
bool canReasonAbout(SVal X) const override {
|
||||
const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
|
||||
|
||||
|
|
@ -971,45 +953,6 @@ public:
|
|||
|
||||
llvm_unreachable("Unsupported expression to reason about!");
|
||||
}
|
||||
|
||||
ProgramStateRef removeDeadBindings(ProgramStateRef State,
|
||||
SymbolReaper &SymReaper) override {
|
||||
ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
|
||||
ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
|
||||
|
||||
for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
|
||||
if (SymReaper.maybeDead(I->first))
|
||||
CZ = CZFactory.remove(CZ, *I);
|
||||
}
|
||||
|
||||
return State->set<ConstraintZ3>(CZ);
|
||||
}
|
||||
|
||||
ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
|
||||
const SMTExprRef &Exp) override {
|
||||
// Check the model, avoid simplifying AST to save time
|
||||
if (checkModel(State, Exp).isConstrainedTrue())
|
||||
return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
|
||||
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
//==------------------------------------------------------------------------==/
|
||||
// Pretty-printing.
|
||||
//==------------------------------------------------------------------------==/
|
||||
|
||||
void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
|
||||
const char *sep) override {
|
||||
|
||||
ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
|
||||
|
||||
OS << nl << sep << "Constraints:";
|
||||
for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
|
||||
OS << nl << ' ' << I->first << " : ";
|
||||
I->second.print(OS);
|
||||
}
|
||||
OS << nl;
|
||||
}
|
||||
}; // end class Z3ConstraintManager
|
||||
|
||||
} // end anonymous namespace
|
||||
|
|
|
|||
Loading…
Reference in New Issue