Enhance GRBranchNodeBuilderImpl (part of GRCoreEngine) to understand the case

where the true or false CFGBlock* for a branch could be NULL. This will handle
the case where we can determine during CFG construction that a branch is
infeasible.

llvm-svn: 76450
This commit is contained in:
Ted Kremenek 2009-07-20 18:44:36 +00:00
parent 289dfc5e34
commit af9f362840
3 changed files with 38 additions and 14 deletions

View File

@ -311,12 +311,15 @@ class GRBranchNodeBuilderImpl {
bool GeneratedTrue; bool GeneratedTrue;
bool GeneratedFalse; bool GeneratedFalse;
bool InFeasibleTrue;
bool InFeasibleFalse;
public: public:
GRBranchNodeBuilderImpl(CFGBlock* src, CFGBlock* dstT, CFGBlock* dstF, GRBranchNodeBuilderImpl(CFGBlock* src, CFGBlock* dstT, CFGBlock* dstF,
ExplodedNodeImpl* pred, GRCoreEngineImpl* e) ExplodedNodeImpl* pred, GRCoreEngineImpl* e)
: Eng(*e), Src(src), DstT(dstT), DstF(dstF), Pred(pred), : Eng(*e), Src(src), DstT(dstT), DstF(dstF), Pred(pred),
GeneratedTrue(false), GeneratedFalse(false) {} GeneratedTrue(false), GeneratedFalse(false),
InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {}
~GRBranchNodeBuilderImpl(); ~GRBranchNodeBuilderImpl();
@ -331,8 +334,14 @@ public:
} }
void markInfeasible(bool branch) { void markInfeasible(bool branch) {
if (branch) GeneratedTrue = true; if (branch)
else GeneratedFalse = true; InFeasibleTrue = GeneratedTrue = true;
else
InFeasibleFalse = GeneratedFalse = true;
}
bool isFeasible(bool branch) {
return branch ? !InFeasibleTrue : !InFeasibleFalse;
} }
}; };
@ -374,6 +383,10 @@ public:
void markInfeasible(bool branch) { void markInfeasible(bool branch) {
NB.markInfeasible(branch); NB.markInfeasible(branch);
} }
bool isFeasible(bool branch) {
return NB.isFeasible(branch);
}
}; };
class GRIndirectGotoNodeBuilderImpl { class GRIndirectGotoNodeBuilderImpl {

View File

@ -453,6 +453,11 @@ GRStmtNodeBuilderImpl::generateNodeImpl(PostStmt Loc, const void* State,
ExplodedNodeImpl* GRBranchNodeBuilderImpl::generateNodeImpl(const void* State, ExplodedNodeImpl* GRBranchNodeBuilderImpl::generateNodeImpl(const void* State,
bool branch) { bool branch) {
// If the branch has been marked infeasible we should not generate a node.
if (!isFeasible(branch))
return NULL;
bool IsNew; bool IsNew;
ExplodedNodeImpl* Succ = ExplodedNodeImpl* Succ =
@ -460,8 +465,10 @@ ExplodedNodeImpl* GRBranchNodeBuilderImpl::generateNodeImpl(const void* State,
Succ->addPredecessor(Pred); Succ->addPredecessor(Pred);
if (branch) GeneratedTrue = true; if (branch)
else GeneratedFalse = true; GeneratedTrue = true;
else
GeneratedFalse = true;
if (IsNew) { if (IsNew) {
Deferred.push_back(Succ); Deferred.push_back(Succ);

View File

@ -706,16 +706,20 @@ void GRExprEngine::ProcessBranch(Stmt* Condition, Stmt* Term,
} }
// Process the true branch. // Process the true branch.
if (builder.isFeasible(true)) {
if (const GRState *state = PrevState->assume(V, true)) if (const GRState *state = PrevState->assume(V, true))
builder.generateNode(MarkBranch(state, Term, true), true); builder.generateNode(MarkBranch(state, Term, true), true);
else else
builder.markInfeasible(true); builder.markInfeasible(true);
}
// Process the false branch. // Process the false branch.
if (builder.isFeasible(false)) {
if (const GRState *state = PrevState->assume(V, false)) if (const GRState *state = PrevState->assume(V, false))
builder.generateNode(MarkBranch(state, Term, false), false); builder.generateNode(MarkBranch(state, Term, false), false);
else else
builder.markInfeasible(false); builder.markInfeasible(false);
}
} }
/// ProcessIndirectGoto - Called by GRCoreEngine. Used to generate successor /// ProcessIndirectGoto - Called by GRCoreEngine. Used to generate successor