ConstraintManager::AssumeDual now accepts a 'DefinedSVal' instead of 'SVal' for

the condition. This eliminates a source of bugs where the client doesn't
correctly reason about undefined or unknown values. This fixes PR 4759.

llvm-svn: 79952
This commit is contained in:
Ted Kremenek 2009-08-24 22:47:34 +00:00
parent d64be8201d
commit d6cfbafd3b
3 changed files with 9 additions and 4 deletions

View File

@ -37,7 +37,7 @@ public:
SVal UpperBound, bool Assumption) = 0;
std::pair<const GRState*, const GRState*> AssumeDual(const GRState *state,
SVal Cond) {
DefinedSVal Cond) {
return std::make_pair(Assume(state, Cond, true),
Assume(state, Cond, false));
}

View File

@ -177,7 +177,7 @@ class DefinedSVal : public SVal {
protected:
DefinedSVal(const void* d, bool isLoc, unsigned ValKind)
: SVal(d, isLoc, ValKind) {}
public:
// Implement isa<T> support.
static inline bool classof(const SVal *V) {
return !V->isUnknownOrUndef();

View File

@ -575,10 +575,15 @@ public:
if (!Att->isNonNull(idx))
continue;
const SVal &V = state->getSVal(*I);
const DefinedSVal *DV = dyn_cast<DefinedSVal>(&V);
if (!DV)
continue;
ConstraintManager &CM = C.getConstraintManager();
const GRState *stateNotNull, *stateNull;
llvm::tie(stateNotNull, stateNull) = CM.AssumeDual(state,
state->getSVal(*I));
llvm::tie(stateNotNull, stateNull) = CM.AssumeDual(state, *DV);
if (stateNull && !stateNotNull) {
// Generate an error node. Check for a null node in case