aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTed Kremenek <kremenek@apple.com>2011-04-03 04:34:49 +0000
committerTed Kremenek <kremenek@apple.com>2011-04-03 04:34:49 +0000
commit8083414ee7cc8f5c807ed6a4e120fb4e0ab50ff8 (patch)
tree2be30b600c5d1c0b1d5fbff3f94f8cbddbc80c02
parent45fa623886dfb6a23b3cfd6d8764e05884382180 (diff)
static analyzer: Add a new ProgramPoint PostCondition to represent the post position of a branch condition, and a new generateNode method to BranchNodeBuilder using PostCondition ProgramPoint. This method generates a new ExplodedNode but not a new block edge.
Patch by Lei Zhang! git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@128784 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--include/clang/Analysis/ProgramPoint.h13
-rw-r--r--include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h2
-rw-r--r--lib/StaticAnalyzer/Core/CoreEngine.cpp19
3 files changed, 33 insertions, 1 deletions
diff --git a/include/clang/Analysis/ProgramPoint.h b/include/clang/Analysis/ProgramPoint.h
index 54cfc3dc0d..07b4dea987 100644
--- a/include/clang/Analysis/ProgramPoint.h
+++ b/include/clang/Analysis/ProgramPoint.h
@@ -43,6 +43,7 @@ public:
PostStoreKind,
PostPurgeDeadSymbolsKind,
PostStmtCustomKind,
+ PostConditionKind,
PostLValueKind,
PostInitializerKind,
CallEnterKind,
@@ -221,7 +222,17 @@ public:
}
};
-
+// PostCondition represents the post program point of a branch condition.
+class PostCondition : public PostStmt {
+public:
+ PostCondition(const Stmt* S, const LocationContext *L, const void *tag = 0)
+ : PostStmt(S, PostConditionKind, L, tag) {}
+
+ static bool classof(const ProgramPoint* Location) {
+ return Location->getKind() == PostConditionKind;
+ }
+};
+
class LocationCheck : public StmtPoint {
protected:
LocationCheck(const Stmt *S, const LocationContext *L,
diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h b/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
index 41d7b9eafd..9b1402fb3e 100644
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
@@ -307,6 +307,8 @@ public:
BlockCounter getBlockCounter() const { return Eng.WList->getBlockCounter();}
+ ExplodedNode* generateNode(const Stmt *Condition, const GRState* State);
+
ExplodedNode* generateNode(const GRState* State, bool branch);
const CFGBlock* getTargetBlock(bool branch) const {
diff --git a/lib/StaticAnalyzer/Core/CoreEngine.cpp b/lib/StaticAnalyzer/Core/CoreEngine.cpp
index 73709e39d0..a161f652a6 100644
--- a/lib/StaticAnalyzer/Core/CoreEngine.cpp
+++ b/lib/StaticAnalyzer/Core/CoreEngine.cpp
@@ -602,6 +602,25 @@ StmtNodeBuilder::generateNodeInternal(const ProgramPoint &Loc,
return NULL;
}
+// This function generate a new ExplodedNode but not a new branch(block edge).
+ExplodedNode* BranchNodeBuilder::generateNode(const Stmt* Condition,
+ const GRState* State) {
+ bool IsNew;
+
+ ExplodedNode* Succ
+ = Eng.G->getNode(PostCondition(Condition, Pred->getLocationContext()), State,
+ &IsNew);
+
+ Succ->addPredecessor(Pred, *Eng.G);
+
+ Pred = Succ;
+
+ if (IsNew)
+ return Succ;
+
+ return NULL;
+}
+
ExplodedNode* BranchNodeBuilder::generateNode(const GRState* State,
bool branch) {