bool GeneratedTrue;
bool GeneratedFalse;
+ bool InFeasibleTrue;
+ bool InFeasibleFalse;
public:
GRBranchNodeBuilderImpl(CFGBlock* src, CFGBlock* dstT, CFGBlock* dstF,
ExplodedNodeImpl* pred, GRCoreEngineImpl* e)
: Eng(*e), Src(src), DstT(dstT), DstF(dstF), Pred(pred),
- GeneratedTrue(false), GeneratedFalse(false) {}
+ GeneratedTrue(false), GeneratedFalse(false),
+ InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {}
~GRBranchNodeBuilderImpl();
}
void markInfeasible(bool branch) {
- if (branch) GeneratedTrue = true;
- else GeneratedFalse = true;
+ if (branch)
+ InFeasibleTrue = GeneratedTrue = true;
+ else
+ InFeasibleFalse = GeneratedFalse = true;
+ }
+
+ bool isFeasible(bool branch) {
+ return branch ? !InFeasibleTrue : !InFeasibleFalse;
}
};
void markInfeasible(bool branch) {
NB.markInfeasible(branch);
}
+
+ bool isFeasible(bool branch) {
+ return NB.isFeasible(branch);
+ }
};
class GRIndirectGotoNodeBuilderImpl {
}
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;
ExplodedNodeImpl* Succ =
Succ->addPredecessor(Pred);
- if (branch) GeneratedTrue = true;
- else GeneratedFalse = true;
+ if (branch)
+ GeneratedTrue = true;
+ else
+ GeneratedFalse = true;
if (IsNew) {
Deferred.push_back(Succ);
}
// Process the true branch.
- if (const GRState *state = PrevState->assume(V, true))
- builder.generateNode(MarkBranch(state, Term, true), true);
- else
- builder.markInfeasible(true);
+ if (builder.isFeasible(true)) {
+ if (const GRState *state = PrevState->assume(V, true))
+ builder.generateNode(MarkBranch(state, Term, true), true);
+ else
+ builder.markInfeasible(true);
+ }
// Process the false branch.
- if (const GRState *state = PrevState->assume(V, false))
- builder.generateNode(MarkBranch(state, Term, false), false);
- else
- builder.markInfeasible(false);
+ if (builder.isFeasible(false)) {
+ if (const GRState *state = PrevState->assume(V, false))
+ builder.generateNode(MarkBranch(state, Term, false), false);
+ else
+ builder.markInfeasible(false);
+ }
}
/// ProcessIndirectGoto - Called by GRCoreEngine. Used to generate successor