diff options
-rw-r--r-- | include/clang/Analysis/ProgramPoint.h | 13 | ||||
-rw-r--r-- | include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h | 2 | ||||
-rw-r--r-- | lib/StaticAnalyzer/Core/CoreEngine.cpp | 19 |
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) { |