From: Ted Kremenek Date: Fri, 18 Apr 2008 17:20:23 +0000 (+0000) Subject: Added "EvalAssume" virtual method to GRTransferFuncs; this is for evaluating X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=550a0f94938817e3550d79adcc6f1f27410f7593;p=clang Added "EvalAssume" virtual method to GRTransferFuncs; this is for evaluating the checker-specific logic of symbolic assumptions. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@49910 91177308-0d34-0410-b5e6-96231b3b80d8 --- diff --git a/include/clang/Analysis/PathSensitive/GRExprEngine.h b/include/clang/Analysis/PathSensitive/GRExprEngine.h index 0d26d98ad0..46ff661959 100644 --- a/include/clang/Analysis/PathSensitive/GRExprEngine.h +++ b/include/clang/Analysis/PathSensitive/GRExprEngine.h @@ -447,10 +447,16 @@ protected: ValueState* Assume(ValueState* St, LVal Cond, bool Assumption, bool& isFeasible); - + + ValueState* AssumeAux(ValueState* St, LVal Cond, bool Assumption, + bool& isFeasible); + ValueState* Assume(ValueState* St, NonLVal Cond, bool Assumption, bool& isFeasible); + ValueState* AssumeAux(ValueState* St, NonLVal Cond, bool Assumption, + bool& isFeasible); + ValueState* AssumeSymNE(ValueState* St, SymbolID sym, const llvm::APSInt& V, bool& isFeasible); diff --git a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h index d49144f355..60492b5eea 100644 --- a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h +++ b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h @@ -96,6 +96,16 @@ public: GRStmtNodeBuilder& Builder, ReturnStmt* S, ExplodedNode* 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 diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp index 418129caa9..e3fe239553 100644 --- a/lib/Analysis/GRExprEngine.cpp +++ b/lib/Analysis/GRExprEngine.cpp @@ -1840,13 +1840,20 @@ void GRExprEngine::HandleUndefinedStore(Stmt* S, NodeTy* Pred) { //===----------------------------------------------------------------------===// ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond, - bool Assumption, - bool& isFeasible) { + bool Assumption, 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()) { default: assert (false && "'Assume' not implemented for this LVal."); return St; - + case lval::SymbolValKind: if (Assumption) return AssumeSymNE(St, cast(Cond).getSymbol(), @@ -1854,8 +1861,8 @@ ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond, else return AssumeSymEQ(St, cast(Cond).getSymbol(), BasicVals.getZeroWithPtrWidth(), isFeasible); - - + + case lval::DeclValKind: case lval::FuncValKind: case lval::GotoLabelKind: @@ -1871,8 +1878,14 @@ ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond, } ValueState* GRExprEngine::Assume(ValueState* St, NonLVal Cond, - bool Assumption, - bool& isFeasible) { + bool Assumption, 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()) { default: assert (false && "'Assume' not implemented for this NonLVal.");