forked from OSchip/llvm-project
Added "EvalAssume" virtual method to GRTransferFuncs; this is for evaluating
the checker-specific logic of symbolic assumptions. llvm-svn: 49910
This commit is contained in:
parent
65bea23674
commit
3388381993
|
@ -447,10 +447,16 @@ protected:
|
||||||
|
|
||||||
ValueState* Assume(ValueState* St, LVal Cond, bool Assumption,
|
ValueState* Assume(ValueState* St, LVal Cond, bool Assumption,
|
||||||
bool& isFeasible);
|
bool& isFeasible);
|
||||||
|
|
||||||
|
ValueState* AssumeAux(ValueState* St, LVal Cond, bool Assumption,
|
||||||
|
bool& isFeasible);
|
||||||
|
|
||||||
ValueState* Assume(ValueState* St, NonLVal Cond, bool Assumption,
|
ValueState* Assume(ValueState* St, NonLVal Cond, bool Assumption,
|
||||||
bool& isFeasible);
|
bool& isFeasible);
|
||||||
|
|
||||||
|
ValueState* AssumeAux(ValueState* St, NonLVal Cond, bool Assumption,
|
||||||
|
bool& isFeasible);
|
||||||
|
|
||||||
ValueState* AssumeSymNE(ValueState* St, SymbolID sym, const llvm::APSInt& V,
|
ValueState* AssumeSymNE(ValueState* St, SymbolID sym, const llvm::APSInt& V,
|
||||||
bool& isFeasible);
|
bool& isFeasible);
|
||||||
|
|
||||||
|
|
|
@ -96,6 +96,16 @@ public:
|
||||||
GRStmtNodeBuilder<ValueState>& Builder,
|
GRStmtNodeBuilder<ValueState>& Builder,
|
||||||
ReturnStmt* S,
|
ReturnStmt* S,
|
||||||
ExplodedNode<ValueState>* Pred) {}
|
ExplodedNode<ValueState>* Pred) {}
|
||||||
|
|
||||||
|
// Assumptions.
|
||||||
|
|
||||||
|
virtual ValueState* EvalAssume(ValueState* St, NonLVal Cond, bool Assumption){
|
||||||
|
return St;
|
||||||
|
}
|
||||||
|
|
||||||
|
virtual ValueState* EvalAssume(ValueState* St, LVal Cond, bool Assumption) {
|
||||||
|
return St;
|
||||||
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
} // end clang namespace
|
} // end clang namespace
|
||||||
|
|
|
@ -1840,13 +1840,20 @@ void GRExprEngine::HandleUndefinedStore(Stmt* S, NodeTy* Pred) {
|
||||||
//===----------------------------------------------------------------------===//
|
//===----------------------------------------------------------------------===//
|
||||||
|
|
||||||
ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond,
|
ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond,
|
||||||
bool Assumption,
|
bool Assumption, bool& isFeasible) {
|
||||||
bool& isFeasible) {
|
|
||||||
|
St = AssumeAux(St, Cond, Assumption, isFeasible);
|
||||||
|
return isFeasible ? St : TF->EvalAssume(St, Cond, Assumption);
|
||||||
|
}
|
||||||
|
|
||||||
|
ValueState* GRExprEngine::AssumeAux(ValueState* St, LVal Cond,
|
||||||
|
bool Assumption, bool& isFeasible) {
|
||||||
|
|
||||||
switch (Cond.getSubKind()) {
|
switch (Cond.getSubKind()) {
|
||||||
default:
|
default:
|
||||||
assert (false && "'Assume' not implemented for this LVal.");
|
assert (false && "'Assume' not implemented for this LVal.");
|
||||||
return St;
|
return St;
|
||||||
|
|
||||||
case lval::SymbolValKind:
|
case lval::SymbolValKind:
|
||||||
if (Assumption)
|
if (Assumption)
|
||||||
return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
|
return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
|
||||||
|
@ -1854,8 +1861,8 @@ ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond,
|
||||||
else
|
else
|
||||||
return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
|
return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
|
||||||
BasicVals.getZeroWithPtrWidth(), isFeasible);
|
BasicVals.getZeroWithPtrWidth(), isFeasible);
|
||||||
|
|
||||||
|
|
||||||
case lval::DeclValKind:
|
case lval::DeclValKind:
|
||||||
case lval::FuncValKind:
|
case lval::FuncValKind:
|
||||||
case lval::GotoLabelKind:
|
case lval::GotoLabelKind:
|
||||||
|
@ -1871,8 +1878,14 @@ ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond,
|
||||||
}
|
}
|
||||||
|
|
||||||
ValueState* GRExprEngine::Assume(ValueState* St, NonLVal Cond,
|
ValueState* GRExprEngine::Assume(ValueState* St, NonLVal Cond,
|
||||||
bool Assumption,
|
bool Assumption, bool& isFeasible) {
|
||||||
bool& isFeasible) {
|
|
||||||
|
St = AssumeAux(St, Cond, Assumption, isFeasible);
|
||||||
|
return isFeasible ? St : TF->EvalAssume(St, Cond, Assumption);
|
||||||
|
}
|
||||||
|
|
||||||
|
ValueState* GRExprEngine::AssumeAux(ValueState* St, NonLVal Cond,
|
||||||
|
bool Assumption, bool& isFeasible) {
|
||||||
switch (Cond.getSubKind()) {
|
switch (Cond.getSubKind()) {
|
||||||
default:
|
default:
|
||||||
assert (false && "'Assume' not implemented for this NonLVal.");
|
assert (false && "'Assume' not implemented for this NonLVal.");
|
||||||
|
|
Loading…
Reference in New Issue