Added transfer function support for checking for divide-by-zero errors.

llvm-svn: 47547
This commit is contained in:
Ted Kremenek 2008-02-25 17:51:31 +00:00
parent 896c519d19
commit 6f92e2294a
2 changed files with 70 additions and 4 deletions

View File

@ -850,6 +850,33 @@ void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
BinaryOperator::Opcode Op = B->getOpcode();
if (Op == BinaryOperator::Div) { // Check for divide-by-zero.
// First, "assume" that the denominator is 0.
bool isFeasible = false;
StateTy ZeroSt = Assume(St, RightV, false, isFeasible);
if (isFeasible) {
NodeTy* DivZeroNode = Builder->generateNode(B, ZeroSt, N2);
if (DivZeroNode) {
DivZeroNode->markAsSink();
DivZeroes.insert(DivZeroNode);
}
}
// Second, "assume" that the denominator cannot be 0.
isFeasible = false;
St = Assume(St, RightV, true, isFeasible);
if (!isFeasible)
continue;
// Fall-through. The logic below processes the divide.
}
if (Op <= BinaryOperator::Or) {
// Process non-assignements except commas or short-circuited
@ -964,8 +991,35 @@ void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
RightV = EvalCast(RightV, CTy);
// Evaluate operands and promote to result type.
if (Op == BinaryOperator::Div) { // Check for divide-by-zero.
// First, "assume" that the denominator is 0.
bool isFeasible = false;
StateTy ZeroSt = Assume(St, RightV, false, isFeasible);
if (isFeasible) {
NodeTy* DivZeroNode = Builder->generateNode(B, ZeroSt, N2);
if (DivZeroNode) {
DivZeroNode->markAsSink();
DivZeroes.insert(DivZeroNode);
}
}
// Second, "assume" that the denominator cannot be 0.
isFeasible = false;
St = Assume(St, RightV, true, isFeasible);
if (!isFeasible)
continue;
// Fall-through. The logic below processes the divide.
}
RVal Result = EvalCast(EvalBinOp(Op, V, RightV), B->getType());
St = SetRVal(SetRVal(St, B, Result), LeftLV, Result);
}
}

View File

@ -114,18 +114,30 @@ protected:
/// taking a branch based on an uninitialized value.
typedef llvm::SmallPtrSet<NodeTy*,5> UninitBranchesTy;
UninitBranchesTy UninitBranches;
typedef llvm::SmallPtrSet<NodeTy*,5> UninitStoresTy;
typedef llvm::SmallPtrSet<NodeTy*,5> BadDerefTy;
typedef llvm::SmallPtrSet<NodeTy*,5> DivZerosTy;
/// UninitStores - Sinks in the ExplodedGraph that result from
/// making a store to an uninitialized lvalue.
typedef llvm::SmallPtrSet<NodeTy*,5> UninitStoresTy;
UninitStoresTy UninitStores;
/// ImplicitNullDeref - Nodes in the ExplodedGraph that result from
/// taking a dereference on a symbolic pointer that may be NULL.
typedef llvm::SmallPtrSet<NodeTy*,5> BadDerefTy;
/// taking a dereference on a symbolic pointer that MAY be NULL.
BadDerefTy ImplicitNullDeref;
/// ExplicitNullDeref - Nodes in the ExplodedGraph that result from
/// taking a dereference on a symbolic pointer that MUST be NULL.
BadDerefTy ExplicitNullDeref;
/// UnitDeref - Nodes in the ExplodedGraph that result from
/// taking a dereference on an uninitialized value.
BadDerefTy UninitDeref;
/// DivZeroes - Nodes in the ExplodedGraph that result from evaluating
/// a divide-by-zero.
DivZerosTy DivZeroes;
bool StateCleaned;