replica
/
hanchenye-llvm-project
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Move GRTransferFunc* into ValueStateManager, and move the assumption logic there as well. 

llvm-svn: 53743
This commit is contained in:
Ted Kremenek 2008-07-17 23:15:45 +00:00
parent 9976888190
commit 9c32a1ecf5
5 changed files with 245 additions and 230 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
clang/include/clang/Analysis/PathSensitive/GRExprEngine.h
View File

@ -70,10 +70,6 @@ protected:
/// ValueMgr - Object that manages the data for all created RVals.
BasicValueFactory& BasicVals;
/// TF - Object that represents a bundle of transfer functions
/// for manipulating and creating RVals.
GRTransferFuncs* TF;
/// BugTypes - Objects used for reporting bugs.
typedef std::vector<BugType*> BugTypeSet;
BugTypeSet BugTypes;
@ -187,6 +183,8 @@ public:
/// getCFG - Returns the CFG associated with this analysis.
CFG& getCFG() { return G.getCFG(); }
GRTransferFuncs& getTF() { return *StateMgr.TF; }
/// setTransferFunctions
void setTransferFunctions(GRTransferFuncs* tf);
@ -371,7 +369,7 @@ public:
/// ProcessEndPath - Called by GRCoreEngine. Used to generate end-of-path
/// nodes when the control reaches the end of a function.
void ProcessEndPath(EndPathNodeBuilder& builder) {
TF->EvalEndPath(*this, builder);
getTF().EvalEndPath(*this, builder);
}
ValueStateManager& getStateManager() { return StateMgr; }
@ -433,39 +431,14 @@ protected:
/// is true or false.
const ValueState* Assume(const ValueState* St, RVal Cond, bool Assumption,
bool& isFeasible) {
if (Cond.isUnknown()) {
isFeasible = true;
return St;
}
if (isa<LVal>(Cond))
return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
else
return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
return StateMgr.Assume(St, Cond, Assumption, isFeasible);
}
const ValueState* Assume(const ValueState* St, LVal Cond, bool Assumption,
bool& isFeasible);
const ValueState* AssumeAux(const ValueState* St, LVal Cond, bool Assumption,
bool& isFeasible);
bool& isFeasible) {
return StateMgr.Assume(St, Cond, Assumption, isFeasible);
}
const ValueState* Assume(const ValueState* St, NonLVal Cond, bool Assumption,
bool& isFeasible);
const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
bool Assumption, bool& isFeasible);
const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible);
const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible);
const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
const SymIntConstraint& C, bool& isFeasible);
NodeTy* MakeNode(NodeSet& Dst, Stmt* S, NodeTy* Pred, const ValueState* St) {
assert (Builder && "GRStmtNodeBuilder not present.");
return Builder->MakeNode(Dst, S, Pred, St);
@ -560,25 +533,25 @@ protected:
return X;
if (isa<LVal>(X))
return TF->EvalCast(*this, cast<LVal>(X), CastT);
return getTF().EvalCast(*this, cast<LVal>(X), CastT);
else
return TF->EvalCast(*this, cast<NonLVal>(X), CastT);
return getTF().EvalCast(*this, cast<NonLVal>(X), CastT);
}
RVal EvalMinus(UnaryOperator* U, RVal X) {
return X.isValid() ? TF->EvalMinus(*this, U, cast<NonLVal>(X)) : X;
return X.isValid() ? getTF().EvalMinus(*this, U, cast<NonLVal>(X)) : X;
}
RVal EvalComplement(RVal X) {
return X.isValid() ? TF->EvalComplement(*this, cast<NonLVal>(X)) : X;
return X.isValid() ? getTF().EvalComplement(*this, cast<NonLVal>(X)) : X;
}
RVal EvalBinOp(BinaryOperator::Opcode Op, NonLVal L, RVal R) {
return R.isValid() ? TF->EvalBinOp(*this, Op, L, cast<NonLVal>(R)) : R;
return R.isValid() ? getTF().EvalBinOp(*this, Op, L, cast<NonLVal>(R)) : R;
}
RVal EvalBinOp(BinaryOperator::Opcode Op, NonLVal L, NonLVal R) {
return R.isValid() ? TF->EvalBinOp(*this, Op, L, R) : R;
return R.isValid() ? getTF().EvalBinOp(*this, Op, L, R) : R;
}
RVal EvalBinOp(BinaryOperator::Opcode Op, RVal L, RVal R) {
@ -591,9 +564,9 @@ protected:
if (isa<LVal>(L)) {
if (isa<LVal>(R))
return TF->EvalBinOp(*this, Op, cast<LVal>(L), cast<LVal>(R));
return getTF().EvalBinOp(*this, Op, cast<LVal>(L), cast<LVal>(R));
else
return TF->EvalBinOp(*this, Op, cast<LVal>(L), cast<NonLVal>(R));
return getTF().EvalBinOp(*this, Op, cast<LVal>(L), cast<NonLVal>(R));
}
if (isa<LVal>(R)) {
@ -603,10 +576,10 @@ protected:
assert (Op == BinaryOperator::Add || Op == BinaryOperator::Sub);
// Commute the operands.
return TF->EvalBinOp(*this, Op, cast<LVal>(R), cast<NonLVal>(L));
return getTF().EvalBinOp(*this, Op, cast<LVal>(R), cast<NonLVal>(L));
}
else
return TF->EvalBinOp(*this, Op, cast<NonLVal>(L), cast<NonLVal>(R));
return getTF().EvalBinOp(*this, Op, cast<NonLVal>(L), cast<NonLVal>(R));
}
void EvalBinOp(ExplodedNodeSet<ValueState>& Dst, Expr* E,
@ -615,12 +588,12 @@ protected:
void EvalCall(NodeSet& Dst, CallExpr* CE, RVal L, NodeTy* Pred) {
assert (Builder && "GRStmtNodeBuilder must be defined.");
TF->EvalCall(Dst, *this, *Builder, CE, L, Pred);
getTF().EvalCall(Dst, *this, *Builder, CE, L, Pred);
}
void EvalObjCMessageExpr(NodeSet& Dst, ObjCMessageExpr* ME, NodeTy* Pred) {
assert (Builder && "GRStmtNodeBuilder must be defined.");
TF->EvalObjCMessageExpr(Dst, *this, *Builder, ME, Pred);
getTF().EvalObjCMessageExpr(Dst, *this, *Builder, ME, Pred);
}
void EvalStore(NodeSet& Dst, Expr* E, NodeTy* Pred, const ValueState* St,

5
clang/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
View File

@ -108,8 +108,7 @@ public:
const ValueState* St,
const ValueStateManager::DeadSymbolsTy& Dead) {}
// Return statements.
// Return statements.
virtual void EvalReturn(ExplodedNodeSet<ValueState>& Dst,
GRExprEngine& Engine,
GRStmtNodeBuilder<ValueState>& Builder,
@ -118,7 +117,7 @@ public:
// Assumptions.
virtual const ValueState* EvalAssume(GRExprEngine& Engine,
virtual const ValueState* EvalAssume(ValueStateManager& VMgr,
const ValueState* St,
RVal Cond, bool Assumption,
bool& isFeasible) {

43
clang/include/clang/Analysis/PathSensitive/ValueState.h
View File

@ -41,6 +41,7 @@
namespace clang {
class ValueStateManager;
class GRTransferFuncs;
//===----------------------------------------------------------------------===//
// ValueState- An ImmutableMap type Stmt*/Decl*/Symbols to RVals.
@ -217,6 +218,10 @@ private:
/// cfg - The CFG for the analyzed function/method.
CFG& cfg;
/// TF - Object that represents a bundle of transfer functions
/// for manipulating and creating RVals.
GRTransferFuncs* TF;
private:
@ -322,6 +327,44 @@ public:
const ValueState* AddNE(const ValueState* St, SymbolID sym,
const llvm::APSInt& V);
// Assumption logic.
const ValueState* Assume(const ValueState* St, RVal Cond, bool Assumption,
bool& isFeasible) {
if (Cond.isUnknown()) {
isFeasible = true;
return St;
}
if (isa<LVal>(Cond))
return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
else
return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
}
const ValueState* Assume(const ValueState* St, LVal Cond, bool Assumption,
bool& isFeasible);
const ValueState* Assume(const ValueState* St, NonLVal Cond, bool Assumption,
bool& isFeasible);
private:
const ValueState* AssumeAux(const ValueState* St, LVal Cond, bool Assumption,
bool& isFeasible);
const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
bool Assumption, bool& isFeasible);
const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible);
const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible);
const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
const SymIntConstraint& C, bool& isFeasible);
};
} // end clang namespace

190
clang/lib/Analysis/GRExprEngine.cpp
View File

@ -123,7 +123,6 @@ GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx,
StateMgr(G.getContext(), CreateBasicStoreManager(G.getAllocator()),
G.getAllocator(), G.getCFG()),
BasicVals(StateMgr.getBasicValueFactory()),
TF(NULL), // FIXME
SymMgr(StateMgr.getSymbolManager()),
CurrentStmt(NULL),
NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL),
@ -178,8 +177,8 @@ void GRExprEngine::EmitWarnings(BugReporterData& BRData) {
}
void GRExprEngine::setTransferFunctions(GRTransferFuncs* tf) {
TF = tf;
TF->RegisterChecks(*this);
StateMgr.TF = tf;
getTF().RegisterChecks(*this);
}
void GRExprEngine::AddCheck(GRSimpleAPICheck* A, Stmt::StmtClass C) {
@ -252,7 +251,7 @@ void GRExprEngine::ProcessStmt(Stmt* S, StmtNodeBuilder& builder) {
SaveAndRestore<bool> OldPurgeDeadSymbols(Builder->PurgingDeadSymbols);
Builder->PurgingDeadSymbols = true;
TF->EvalDeadSymbols(Tmp, *this, *Builder, EntryNode, S,
getTF().EvalDeadSymbols(Tmp, *this, *Builder, EntryNode, S,
CleanedState, DeadSymbols);
if (!Builder->BuildSinks && !Builder->HasGeneratedNode)
@ -964,13 +963,13 @@ void GRExprEngine::EvalStore(NodeSet& Dst, Expr* Ex, NodeTy* Pred,
assert (!location.isUndef());
TF->EvalStore(Dst, *this, *Builder, Ex, Pred, St, location, Val);
getTF().EvalStore(Dst, *this, *Builder, Ex, Pred, St, location, Val);
// Handle the case where no nodes where generated. Auto-generate that
// contains the updated state if we aren't generating sinks.
if (!Builder->BuildSinks && Dst.size() == size && !Builder->HasGeneratedNode)
TF->GRTransferFuncs::EvalStore(Dst, *this, *Builder, Ex, Pred, St,
getTF().GRTransferFuncs::EvalStore(Dst, *this, *Builder, Ex, Pred, St,
location, Val);
}
@ -1939,7 +1938,7 @@ void GRExprEngine::EvalReturn(NodeSet& Dst, ReturnStmt* S, NodeTy* Pred) {
SaveAndRestore<bool> OldSink(Builder->BuildSinks);
SaveOr OldHasGen(Builder->HasGeneratedNode);
TF->EvalReturn(Dst, *this, *Builder, S, Pred);
getTF().EvalReturn(Dst, *this, *Builder, S, Pred);
// Handle the case where no nodes where generated.
@ -2240,184 +2239,13 @@ void GRExprEngine::EvalBinOp(ExplodedNodeSet<ValueState>& Dst, Expr* Ex,
unsigned size = Dst.size();
SaveOr OldHasGen(Builder->HasGeneratedNode);
TF->EvalBinOpNN(Dst, *this, *Builder, Op, Ex, L, R, Pred);
getTF().EvalBinOpNN(Dst, *this, *Builder, Op, Ex, L, R, Pred);
if (!Builder->BuildSinks && Dst.size() == size &&
!Builder->HasGeneratedNode)
MakeNode(Dst, Ex, Pred, GetState(Pred));
}
//===----------------------------------------------------------------------===//
// "Assume" logic.
//===----------------------------------------------------------------------===//
const ValueState* GRExprEngine::Assume(const ValueState* St, LVal Cond,
bool Assumption, bool& isFeasible) {
St = AssumeAux(St, Cond, Assumption, isFeasible);
return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
: St;
}
const ValueState* GRExprEngine::AssumeAux(const ValueState* St, LVal Cond,
bool Assumption, bool& isFeasible) {
switch (Cond.getSubKind()) {
default:
assert (false && "'Assume' not implemented for this LVal.");
return St;
case lval::SymbolValKind:
if (Assumption)
return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
BasicVals.getZeroWithPtrWidth(), isFeasible);
else
return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
BasicVals.getZeroWithPtrWidth(), isFeasible);
case lval::DeclValKind:
case lval::FuncValKind:
case lval::GotoLabelKind:
case lval::StringLiteralValKind:
isFeasible = Assumption;
return St;
case lval::FieldOffsetKind:
return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
Assumption, isFeasible);
case lval::ArrayOffsetKind:
return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
Assumption, isFeasible);
case lval::ConcreteIntKind: {
bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
isFeasible = b ? Assumption : !Assumption;
return St;
}
}
}
const ValueState* GRExprEngine::Assume(const ValueState* St, NonLVal Cond,
bool Assumption, bool& isFeasible) {
St = AssumeAux(St, Cond, Assumption, isFeasible);
return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
: St;
}
const ValueState* GRExprEngine::AssumeAux(const ValueState* St, NonLVal Cond,
bool Assumption, bool& isFeasible) {
switch (Cond.getSubKind()) {
default:
assert (false && "'Assume' not implemented for this NonLVal.");
return St;
case nonlval::SymbolValKind: {
nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
SymbolID sym = SV.getSymbol();
if (Assumption)
return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
isFeasible);
else
return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
isFeasible);
}
case nonlval::SymIntConstraintValKind:
return
AssumeSymInt(St, Assumption,
cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
isFeasible);
case nonlval::ConcreteIntKind: {
bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
isFeasible = b ? Assumption : !Assumption;
return St;
}
case nonlval::LValAsIntegerKind: {
return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
Assumption, isFeasible);
}
}
}
const ValueState* GRExprEngine::AssumeSymNE(const ValueState* St,
SymbolID sym, const llvm::APSInt& V,
bool& isFeasible) {
// First, determine if sym == X, where X != V.
if (const llvm::APSInt* X = St->getSymVal(sym)) {
isFeasible = *X != V;
return St;
}
// Second, determine if sym != V.
if (St->isNotEqual(sym, V)) {
isFeasible = true;
return St;
}
// If we reach here, sym is not a constant and we don't know if it is != V.
// Make that assumption.
isFeasible = true;
return StateMgr.AddNE(St, sym, V);
}
const ValueState* GRExprEngine::AssumeSymEQ(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible) {
// First, determine if sym == X, where X != V.
if (const llvm::APSInt* X = St->getSymVal(sym)) {
isFeasible = *X == V;
return St;
}
// Second, determine if sym != V.
if (St->isNotEqual(sym, V)) {
isFeasible = false;
return St;
}
// If we reach here, sym is not a constant and we don't know if it is == V.
// Make that assumption.
isFeasible = true;
return StateMgr.AddEQ(St, sym, V);
}
const ValueState* GRExprEngine::AssumeSymInt(const ValueState* St,
bool Assumption,
const SymIntConstraint& C,
bool& isFeasible) {
switch (C.getOpcode()) {
default:
// No logic yet for other operators.
isFeasible = true;
return St;
case BinaryOperator::EQ:
if (Assumption)
return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
case BinaryOperator::NE:
if (Assumption)
return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
}
}
//===----------------------------------------------------------------------===//
// Visualization.
//===----------------------------------------------------------------------===//
@ -2733,7 +2561,7 @@ void GRExprEngine::ViewGraph(bool trim) {
else {
GraphPrintCheckerState = this;
GraphPrintSourceManager = &getContext().getSourceManager();
GraphCheckerStatePrinter = TF->getCheckerStatePrinter();
GraphCheckerStatePrinter = getTF().getCheckerStatePrinter();
llvm::ViewGraph(*G.roots_begin(), "GRExprEngine");
@ -2748,7 +2576,7 @@ void GRExprEngine::ViewGraph(NodeTy** Beg, NodeTy** End) {
#ifndef NDEBUG
GraphPrintCheckerState = this;
GraphPrintSourceManager = &getContext().getSourceManager();
GraphCheckerStatePrinter = TF->getCheckerStatePrinter();
GraphCheckerStatePrinter = getTF().getCheckerStatePrinter();
GRExprEngine::GraphTy* TrimmedG = G.Trim(Beg, End);

172
clang/lib/Analysis/ValueState.cpp
View File

@ -13,6 +13,7 @@
#include "clang/Analysis/PathSensitive/ValueState.h"
#include "llvm/ADT/SmallSet.h"
#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
using namespace clang;
@ -294,3 +295,174 @@ void ValueState::print(std::ostream& Out, CheckerStatePrinter* P,
if (P && CheckerState)
P->PrintCheckerState(Out, CheckerState, nl, sep);
}
//===----------------------------------------------------------------------===//
// "Assume" logic.
//===----------------------------------------------------------------------===//
const ValueState* ValueStateManager::Assume(const ValueState* St, LVal Cond,
bool Assumption, bool& isFeasible) {
St = AssumeAux(St, Cond, Assumption, isFeasible);
return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
: St;
}
const ValueState* ValueStateManager::AssumeAux(const ValueState* St, LVal Cond,
bool Assumption, bool& isFeasible) {
switch (Cond.getSubKind()) {
default:
assert (false && "'Assume' not implemented for this LVal.");
return St;
case lval::SymbolValKind:
if (Assumption)
return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
BasicVals.getZeroWithPtrWidth(), isFeasible);
else
return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
BasicVals.getZeroWithPtrWidth(), isFeasible);
case lval::DeclValKind:
case lval::FuncValKind:
case lval::GotoLabelKind:
case lval::StringLiteralValKind:
isFeasible = Assumption;
return St;
case lval::FieldOffsetKind:
return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
Assumption, isFeasible);
case lval::ArrayOffsetKind:
return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
Assumption, isFeasible);
case lval::ConcreteIntKind: {
bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
isFeasible = b ? Assumption : !Assumption;
return St;
}
}
}
const ValueState* ValueStateManager::Assume(const ValueState* St, NonLVal Cond,
bool Assumption, bool& isFeasible) {
St = AssumeAux(St, Cond, Assumption, isFeasible);
return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
: St;
}
const ValueState* ValueStateManager::AssumeAux(const ValueState* St, NonLVal Cond,
bool Assumption, bool& isFeasible) {
switch (Cond.getSubKind()) {
default:
assert (false && "'Assume' not implemented for this NonLVal.");
return St;
case nonlval::SymbolValKind: {
nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
SymbolID sym = SV.getSymbol();
if (Assumption)
return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
isFeasible);
else
return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
isFeasible);
}
case nonlval::SymIntConstraintValKind:
return
AssumeSymInt(St, Assumption,
cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
isFeasible);
case nonlval::ConcreteIntKind: {
bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
isFeasible = b ? Assumption : !Assumption;
return St;
}
case nonlval::LValAsIntegerKind: {
return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
Assumption, isFeasible);
}
}
}
const ValueState* ValueStateManager::AssumeSymNE(const ValueState* St,
SymbolID sym, const llvm::APSInt& V,
bool& isFeasible) {
// First, determine if sym == X, where X != V.
if (const llvm::APSInt* X = St->getSymVal(sym)) {
isFeasible = *X != V;
return St;
}
// Second, determine if sym != V.
if (St->isNotEqual(sym, V)) {
isFeasible = true;
return St;
}
// If we reach here, sym is not a constant and we don't know if it is != V.
// Make that assumption.
isFeasible = true;
return AddNE(St, sym, V);
}
const ValueState* ValueStateManager::AssumeSymEQ(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible) {
// First, determine if sym == X, where X != V.
if (const llvm::APSInt* X = St->getSymVal(sym)) {
isFeasible = *X == V;
return St;
}
// Second, determine if sym != V.
if (St->isNotEqual(sym, V)) {
isFeasible = false;
return St;
}
// If we reach here, sym is not a constant and we don't know if it is == V.
// Make that assumption.
isFeasible = true;
return AddEQ(St, sym, V);
}
const ValueState* ValueStateManager::AssumeSymInt(const ValueState* St,
bool Assumption,
const SymIntConstraint& C,
bool& isFeasible) {
switch (C.getOpcode()) {
default:
// No logic yet for other operators.
isFeasible = true;
return St;
case BinaryOperator::EQ:
if (Assumption)
return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
case BinaryOperator::NE:
if (Assumption)
return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
}
}