diff options
author | Jordy Rose <jediknil@belkadan.com> | 2010-08-16 20:34:06 +0000 |
---|---|---|
committer | Jordy Rose <jediknil@belkadan.com> | 2010-08-16 20:34:06 +0000 |
commit | 1802eebad8ebbd0b771b0776dbc53d2208af46d1 (patch) | |
tree | bef26dfbdc97ee0f02cf7bf8be0d55bcada6cc13 /lib/Checker/GRState.cpp | |
parent | 697ca6dc944fd1233a6f07f0777807fbab6a31c1 (diff) |
Move GRState::AssumeInBound out of its header file -- it's not really inline-friendly anymore.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@111179 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Checker/GRState.cpp')
-rw-r--r-- | lib/Checker/GRState.cpp | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/lib/Checker/GRState.cpp b/lib/Checker/GRState.cpp index 21811395d8..37ff87abec 100644 --- a/lib/Checker/GRState.cpp +++ b/lib/Checker/GRState.cpp @@ -181,6 +181,50 @@ const GRState *GRState::BindExpr(const Stmt* Ex, SVal V, bool Invalidate) const{ return getStateManager().getPersistentState(NewSt); } +const GRState *GRState::AssumeInBound(DefinedOrUnknownSVal Idx, + DefinedOrUnknownSVal UpperBound, + bool Assumption) const { + if (Idx.isUnknown() || UpperBound.isUnknown()) + return this; + + // Build an expression for 0 <= Idx < UpperBound. + // This is the same as Idx + MIN < UpperBound + MIN, if overflow is allowed. + // FIXME: This should probably be part of SValuator. + GRStateManager &SM = getStateManager(); + ValueManager &VM = SM.getValueManager(); + SValuator &SV = VM.getSValuator(); + ASTContext &Ctx = VM.getContext(); + + // Get the offset: the minimum value of the array index type. + BasicValueFactory &BVF = VM.getBasicValueFactory(); + // FIXME: This should be using ValueManager::ArrayIndexTy...somehow. + QualType IndexTy = Ctx.IntTy; + nonloc::ConcreteInt Min = BVF.getMinValue(IndexTy); + + // Adjust the index. + SVal NewIdx = SV.EvalBinOpNN(this, BinaryOperator::Add, + cast<NonLoc>(Idx), Min, IndexTy); + if (NewIdx.isUnknownOrUndef()) + return this; + + // Adjust the upper bound. + SVal NewBound = SV.EvalBinOpNN(this, BinaryOperator::Add, + cast<NonLoc>(UpperBound), Min, IndexTy); + if (NewBound.isUnknownOrUndef()) + return this; + + // Build the actual comparison. + SVal InBound = SV.EvalBinOpNN(this, BinaryOperator::LT, + cast<NonLoc>(NewIdx), cast<NonLoc>(NewBound), + Ctx.IntTy); + if (InBound.isUnknownOrUndef()) + return this; + + // Finally, let the constraint manager take care of it. + ConstraintManager &CM = SM.getConstraintManager(); + return CM.Assume(this, cast<DefinedSVal>(InBound), Assumption); +} + const GRState* GRStateManager::getInitialState(const LocationContext *InitLoc) { GRState State(this, EnvMgr.getInitialEnvironment(), |