Implemented more boilerplate in GREngine for processing branches. Now
we automatically generate a new successor node along an edge if the checker did not explicitly do so (i.e., we just propagate the current state). llvm-svn: 46536
This commit is contained in:
parent
ee2d5a540c
commit
7ff1893f86
|
@ -831,8 +831,7 @@ public:
|
||||||
|
|
||||||
/// ProcessBranch - Called by GREngine. Used to generate successor
|
/// ProcessBranch - Called by GREngine. Used to generate successor
|
||||||
/// nodes by processing the 'effects' of a branch condition.
|
/// nodes by processing the 'effects' of a branch condition.
|
||||||
void ProcessBranch(Stmt* Condition, Stmt* Term, BranchNodeBuilder& builder)
|
void ProcessBranch(Stmt* Condition, Stmt* Term, BranchNodeBuilder& builder);
|
||||||
{}
|
|
||||||
|
|
||||||
/// RemoveDeadBindings - Return a new state that is the same as 'M' except
|
/// RemoveDeadBindings - Return a new state that is the same as 'M' except
|
||||||
/// that all subexpression mappings are removed and that any
|
/// that all subexpression mappings are removed and that any
|
||||||
|
@ -877,6 +876,12 @@ public:
|
||||||
} // end anonymous namespace
|
} // end anonymous namespace
|
||||||
|
|
||||||
|
|
||||||
|
void GRConstants::ProcessBranch(Stmt* Condition, Stmt* Term,
|
||||||
|
BranchNodeBuilder& builder) {
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
void GRConstants::ProcessStmt(Stmt* S, StmtNodeBuilder& builder) {
|
void GRConstants::ProcessStmt(Stmt* S, StmtNodeBuilder& builder) {
|
||||||
Builder = &builder;
|
Builder = &builder;
|
||||||
|
|
||||||
|
|
|
@ -296,6 +296,14 @@ void GRBranchNodeBuilderImpl::generateNodeImpl(void* State, bool branch) {
|
||||||
|
|
||||||
Succ->addPredecessor(Pred);
|
Succ->addPredecessor(Pred);
|
||||||
|
|
||||||
|
if (branch) GeneratedTrue = true;
|
||||||
|
else GeneratedFalse = true;
|
||||||
|
|
||||||
if (IsNew)
|
if (IsNew)
|
||||||
Eng.WList->Enqueue(GRWorkListUnit(Succ));
|
Eng.WList->Enqueue(GRWorkListUnit(Succ));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
GRBranchNodeBuilderImpl::~GRBranchNodeBuilderImpl() {
|
||||||
|
if (!GeneratedTrue) generateNodeImpl(Pred->State, true);
|
||||||
|
if (!GeneratedFalse) generateNodeImpl(Pred->State, false);
|
||||||
|
}
|
||||||
|
|
|
@ -167,12 +167,16 @@ class GRBranchNodeBuilderImpl {
|
||||||
CFGBlock* DstF;
|
CFGBlock* DstF;
|
||||||
ExplodedNodeImpl* Pred;
|
ExplodedNodeImpl* Pred;
|
||||||
|
|
||||||
|
bool GeneratedTrue;
|
||||||
|
bool GeneratedFalse;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
GRBranchNodeBuilderImpl(CFGBlock* src, CFGBlock* dstT, CFGBlock* dstF,
|
GRBranchNodeBuilderImpl(CFGBlock* src, CFGBlock* dstT, CFGBlock* dstF,
|
||||||
ExplodedNodeImpl* pred, GREngineImpl* e)
|
ExplodedNodeImpl* pred, GREngineImpl* 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) {}
|
||||||
|
|
||||||
~GRBranchNodeBuilderImpl() {}
|
~GRBranchNodeBuilderImpl();
|
||||||
|
|
||||||
const ExplodedGraphImpl& getGraph() const { return *Eng.G; }
|
const ExplodedGraphImpl& getGraph() const { return *Eng.G; }
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue