ExplodedGraph.h revision c77a55126fcad66fb086f8e100a494caa2496a2d
151125a21eafc29c925cac3655b46cfd8ef55f764Ted Kremenek//=-- ExplodedGraph.h - Local, Path-Sens. "Exploded Graph" -*- C++ -*-------==// 24241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// 34241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// The LLVM Compiler Infrastructure 44241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// 54241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// This file is distributed under the University of Illinois Open Source 64241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// License. See LICENSE.TXT for details. 74241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// 84241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek//===----------------------------------------------------------------------===// 94241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// 1051125a21eafc29c925cac3655b46cfd8ef55f764Ted Kremenek// This file defines the template classes ExplodedNode and ExplodedGraph, 1151125a21eafc29c925cac3655b46cfd8ef55f764Ted Kremenek// which represent a path-sensitive, intra-procedural "exploded graph." 12b2213dc3dd8f58b611b91d2fce4834a767efcba7Jeffrey Yasskin// See "Precise interprocedural dataflow analysis via graph reachability" 13b2213dc3dd8f58b611b91d2fce4834a767efcba7Jeffrey Yasskin// by Reps, Horwitz, and Sagiv 14b2213dc3dd8f58b611b91d2fce4834a767efcba7Jeffrey Yasskin// (http://portal.acm.org/citation.cfm?id=199462) for the definition of an 15b2213dc3dd8f58b611b91d2fce4834a767efcba7Jeffrey Yasskin// exploded graph. 164241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// 174241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek//===----------------------------------------------------------------------===// 184241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 194241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#ifndef LLVM_CLANG_ANALYSIS_EXPLODEDGRAPH 204241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#define LLVM_CLANG_ANALYSIS_EXPLODEDGRAPH 214241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 224a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek#include "clang/Analysis/ProgramPoint.h" 231309f9a3b225ea846e5822691c39a77423125505Ted Kremenek#include "clang/Analysis/AnalysisContext.h" 2463bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek#include "clang/AST/Decl.h" 254241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#include "llvm/ADT/SmallVector.h" 264241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#include "llvm/ADT/FoldingSet.h" 27f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek#include "llvm/ADT/SmallPtrSet.h" 284241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#include "llvm/Support/Allocator.h" 29ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek#include "llvm/ADT/OwningPtr.h" 304a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek#include "llvm/ADT/GraphTraits.h" 314a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek#include "llvm/ADT/DepthFirstIterator.h" 3263bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek#include "llvm/Support/Casting.h" 335fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek#include "clang/Analysis/Support/BumpVector.h" 344241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 354241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremeneknamespace clang { 364a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 37c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xuclass GRState; 3811062b118476368fa5b294954713e5df97d8599fTed Kremenekclass CFG; 395fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenekclass ExplodedGraph; 4011062b118476368fa5b294954713e5df97d8599fTed Kremenek 41cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek//===----------------------------------------------------------------------===// 42cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek// ExplodedGraph "implementation" classes. These classes are not typed to 43cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek// contain a specific kind of state. Typed-specialized versions are defined 44cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek// on top of these classes. 45cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek//===----------------------------------------------------------------------===// 461eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 47c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xuclass ExplodedNode : public llvm::FoldingSetNode { 4838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu friend class ExplodedGraph; 490111f575b968e423dccae439e501225b8314b257Zhongxing Xu friend class GRCoreEngine; 50031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRStmtNodeBuilder; 51031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRBranchNodeBuilder; 52031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRIndirectGotoNodeBuilder; 53031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRSwitchNodeBuilder; 541eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump friend class GREndPathNodeBuilder; 551eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 564c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek class NodeGroup { 57b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek enum { Size1 = 0x0, SizeOther = 0x1, AuxFlag = 0x2, Mask = 0x3 }; 584c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek uintptr_t P; 591eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 60ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek unsigned getKind() const { 61596f0a1e54f610926e8bfded9efa1c639f824dedTed Kremenek return P & 0x1; 62ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek } 631eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 64ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek void* getPtr() const { 65ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek assert (!getFlag()); 66b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek return reinterpret_cast<void*>(P & ~Mask); 67ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek } 68ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek 69c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode *getNode() const { 70c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu return reinterpret_cast<ExplodedNode*>(getPtr()); 71ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek } 721eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 734c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek public: 744c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek NodeGroup() : P(0) {} 751eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 765fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek ExplodedNode **begin() const; 771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 785fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek ExplodedNode **end() const; 791eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 805d5480380d7b7c3590a0283ddf239220e514e576Ted Kremenek unsigned size() const; 811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 825fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek bool empty() const { return (P & ~Mask) == 0; } 831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 845fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek void addNode(ExplodedNode* N, ExplodedGraph &G); 851eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 86b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek void setFlag() { 875fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek assert(P == 0); 88ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek P = AuxFlag; 89f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek } 901eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 91b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek bool getFlag() const { 92b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek return P & AuxFlag ? true : false; 93f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek } 941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump }; 951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 964a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// Location - The program location (within a function body) associated 974a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// with this node. 984a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const ProgramPoint Location; 991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1004323a57627e796dcfdfdb7d47672dc09ed308edaTed Kremenek /// State - The state associated with this node. 101c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu const GRState* State; 1021eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1034a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// Preds - The predecessors of this node. 1044c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek NodeGroup Preds; 1051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1064a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// Succs - The successors of this node. 1074c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek NodeGroup Succs; 108c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1094a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenekpublic: 110c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1111eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump explicit ExplodedNode(const ProgramPoint& loc, const GRState* state) 112c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu : Location(loc), State(state) {} 113c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1144a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// getLocation - Returns the edge associated with the given node. 1150f9063c116b7c3b05d8042b5976463c2dae04861Ted Kremenek ProgramPoint getLocation() const { return Location; } 116c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1171eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump const LocationContext *getLocationContext() const { 1181eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump return getLocation().getLocationContext(); 11925e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu } 12025e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu 1215032ffe4259e7d436f2eb19e5a29fdae559e7c12Zhongxing Xu const Decl &getCodeDecl() const { return *getLocationContext()->getDecl(); } 1225032ffe4259e7d436f2eb19e5a29fdae559e7c12Zhongxing Xu 1235032ffe4259e7d436f2eb19e5a29fdae559e7c12Zhongxing Xu CFG &getCFG() const { return *getLocationContext()->getCFG(); } 1245032ffe4259e7d436f2eb19e5a29fdae559e7c12Zhongxing Xu 125b317f8f5ca8737a5bbad97a3f7566a2dbd2ed61bZhongxing Xu ParentMap &getParentMap() const {return getLocationContext()->getParentMap();} 126b317f8f5ca8737a5bbad97a3f7566a2dbd2ed61bZhongxing Xu 127b317f8f5ca8737a5bbad97a3f7566a2dbd2ed61bZhongxing Xu LiveVariables &getLiveVariables() const { 128b317f8f5ca8737a5bbad97a3f7566a2dbd2ed61bZhongxing Xu return *getLocationContext()->getLiveVariables(); 129c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu } 130c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 131b317f8f5ca8737a5bbad97a3f7566a2dbd2ed61bZhongxing Xu const GRState* getState() const { return State; } 132b317f8f5ca8737a5bbad97a3f7566a2dbd2ed61bZhongxing Xu 13352c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek template <typename T> 13452c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek const T* getLocationAs() const { return llvm::dyn_cast<T>(&Location); } 135c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1361eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump static void Profile(llvm::FoldingSetNodeID &ID, 1375fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek const ProgramPoint& Loc, const GRState* state) { 1385fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek ID.Add(Loc); 1395fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek ID.AddPointer(state); 1405fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek } 141c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 142c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu void Profile(llvm::FoldingSetNodeID& ID) const { 143c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu Profile(ID, getLocation(), getState()); 144c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu } 145c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1461eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump /// addPredeccessor - Adds a predecessor to the current node, and 147c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu /// in tandem add this node as a successor of the other node. 1485fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek void addPredecessor(ExplodedNode* V, ExplodedGraph &G); 149c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1504a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek unsigned succ_size() const { return Succs.size(); } 1514a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek unsigned pred_size() const { return Preds.size(); } 1524a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek bool succ_empty() const { return Succs.empty(); } 1530e8a3c743b9b3e3039e329a1736122d3b5b5fed9Ted Kremenek bool pred_empty() const { return Preds.empty(); } 1541eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 155ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek bool isSink() const { return Succs.getFlag(); } 1561eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump void markAsSink() { Succs.setFlag(); } 1574a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 15852c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek ExplodedNode* getFirstPred() { 15952c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek return pred_empty() ? NULL : *(pred_begin()); 16052c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek } 1611eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 16252c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek const ExplodedNode* getFirstPred() const { 16352c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek return const_cast<ExplodedNode*>(this)->getFirstPred(); 16452c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek } 1651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1664a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek // Iterators over successor and predecessor vertices. 1674a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef ExplodedNode** succ_iterator; 1683148eb4a75f70f2636075c364d03104223f004d3Ted Kremenek typedef const ExplodedNode* const * const_succ_iterator; 1694a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef ExplodedNode** pred_iterator; 1703148eb4a75f70f2636075c364d03104223f004d3Ted Kremenek typedef const ExplodedNode* const * const_pred_iterator; 1714a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 172c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu pred_iterator pred_begin() { return Preds.begin(); } 173c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu pred_iterator pred_end() { return Preds.end(); } 1744a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 1754a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_pred_iterator pred_begin() const { 1764a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->pred_begin(); 1771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 1784a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_pred_iterator pred_end() const { 1794a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->pred_end(); 1804a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 1814a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 182c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu succ_iterator succ_begin() { return Succs.begin(); } 183c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu succ_iterator succ_end() { return Succs.end(); } 1844a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 1854a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_succ_iterator succ_begin() const { 1864a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->succ_begin(); 1874a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 1884a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_succ_iterator succ_end() const { 1894a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->succ_end(); 1904a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 191c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 192c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu // For debugging. 1931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 194c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xupublic: 1951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 196c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu class Auditor { 197c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu public: 198c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu virtual ~Auditor(); 199c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu virtual void AddEdge(ExplodedNode* Src, ExplodedNode* Dst) = 0; 200c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu }; 2011eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 202c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu static void SetAuditor(Auditor* A); 203c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu}; 204c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 20538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu// FIXME: Is this class necessary? 20638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xuclass InterExplodedGraphMap { 20738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::DenseMap<const ExplodedNode*, ExplodedNode*> M; 2081eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump friend class ExplodedGraph; 209c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 21038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xupublic: 21138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedNode* getMappedNode(const ExplodedNode* N) const; 2121eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2137177dee8aee4b432911c91f1b788963bec0cac9fDaniel Dunbar InterExplodedGraphMap() {} 21438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu virtual ~InterExplodedGraphMap() {} 2154a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek}; 2164a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 21738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xuclass ExplodedGraph { 2184241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenekprotected: 2190111f575b968e423dccae439e501225b8314b257Zhongxing Xu friend class GRCoreEngine; 220e96de2dfde487211fb52f9139cdcae64d051a406Zhongxing Xu 2214241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek // Type definitions. 222c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef llvm::SmallVector<ExplodedNode*,2> RootsTy; 223c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef llvm::SmallVector<ExplodedNode*,10> EndNodesTy; 2241eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2254241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// Roots - The roots of the simulation graph. Usually there will be only 2264241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// one, but clients are free to establish multiple subgraphs within a single 2274241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// SimulGraph. Moreover, these subgraphs can often merge when paths from 2284241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// different roots reach the same state at the same program location. 2294241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek RootsTy Roots; 2304241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 2314241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// EndNodes - The nodes in the simulation graph which have been 2324241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// specially marked as the endpoint of an abstract simulation path. 2334241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek EndNodesTy EndNodes; 23438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 23538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// Nodes - The nodes in the graph. 23638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::FoldingSet<ExplodedNode> Nodes; 23738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 2385fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek /// BVC - Allocator and context for allocating nodes and their predecessor 2395fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek /// and successor groups. 2405fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek BumpVectorContext BVC; 2411eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 24239b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek /// NumNodes - The number of nodes in the graph. 24339b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek unsigned NumNodes; 2444241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 24538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xupublic: 24638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// getNode - Retrieve the node associated with a (Location,State) pair, 24738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// where the 'Location' is a ProgramPoint in the CFG. If no node for 24838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// this pair exists, it is created. IsNew is set to true if 24938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// the node was freshly created. 25038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 25138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedNode* getNode(const ProgramPoint& L, const GRState *State, 25238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu bool* IsNew = 0); 2531eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 25438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedGraph* MakeEmptyGraph() const { 255c77a55126fcad66fb086f8e100a494caa2496a2dZhongxing Xu return new ExplodedGraph(); 25638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu } 2574a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 2584241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// addRoot - Add an untyped node to the set of roots. 259c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode* addRoot(ExplodedNode* V) { 260ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek Roots.push_back(V); 261ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek return V; 262ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek } 2634241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 2644241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// addEndOfPath - Add an untyped node to the set of EOP nodes. 265c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode* addEndOfPath(ExplodedNode* V) { 266ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek EndNodes.push_back(V); 267ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek return V; 268ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek } 26938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 270c77a55126fcad66fb086f8e100a494caa2496a2dZhongxing Xu ExplodedGraph() : NumNodes(0) {} 2714241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 2725fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek ~ExplodedGraph() {} 2734a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 2744241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek unsigned num_roots() const { return Roots.size(); } 2754a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek unsigned num_eops() const { return EndNodes.size(); } 2761eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 27739b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek bool empty() const { return NumNodes == 0; } 27839b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek unsigned size() const { return NumNodes; } 279c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 2804241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek // Iterators. 28138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef ExplodedNode NodeTy; 28238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef llvm::FoldingSet<ExplodedNode> AllNodesTy; 2837ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek typedef NodeTy** roots_iterator; 28438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef NodeTy* const * const_roots_iterator; 2857ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek typedef NodeTy** eop_iterator; 28638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef NodeTy* const * const_eop_iterator; 28738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef AllNodesTy::iterator node_iterator; 28838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef AllNodesTy::const_iterator const_node_iterator; 2891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 29038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu node_iterator nodes_begin() { return Nodes.begin(); } 2917ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek 29238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu node_iterator nodes_end() { return Nodes.end(); } 2931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 29438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_node_iterator nodes_begin() const { return Nodes.begin(); } 2951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 29638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_node_iterator nodes_end() const { return Nodes.end(); } 2971eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 29838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu roots_iterator roots_begin() { return Roots.begin(); } 2991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 30038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu roots_iterator roots_end() { return Roots.end(); } 3011eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 30238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_roots_iterator roots_begin() const { return Roots.begin(); } 3031eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3041eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump const_roots_iterator roots_end() const { return Roots.end(); } 3054241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 30638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu eop_iterator eop_begin() { return EndNodes.begin(); } 3071eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 30838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu eop_iterator eop_end() { return EndNodes.end(); } 3091eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 31038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_eop_iterator eop_begin() const { return EndNodes.begin(); } 3111eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 31238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_eop_iterator eop_end() const { return EndNodes.end(); } 31338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 3145fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek llvm::BumpPtrAllocator & getAllocator() { return BVC.getAllocator(); } 3155fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek BumpVectorContext &getNodeAllocator() { return BVC; } 31638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 31738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef llvm::DenseMap<const ExplodedNode*, ExplodedNode*> NodeMap; 31838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 319c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu std::pair<ExplodedGraph*, InterExplodedGraphMap*> 320fe9e543a2a363df7fcaa899367d3b2580b63b27cTed Kremenek Trim(const NodeTy* const* NBeg, const NodeTy* const* NEnd, 32138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::DenseMap<const void*, const void*> *InverseMap = 0) const; 322cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek 32338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedGraph* TrimInternal(const ExplodedNode* const * NBeg, 32438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const ExplodedNode* const * NEnd, 32538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu InterExplodedGraphMap *M, 32638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::DenseMap<const void*, const void*> *InverseMap) const; 3274241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek}; 328cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek 329f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenekclass ExplodedNodeSet { 330c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef llvm::SmallPtrSet<ExplodedNode*,5> ImplTy; 331f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek ImplTy Impl; 3321eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 333f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenekpublic: 334c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNodeSet(ExplodedNode* N) { 335c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu assert (N && !static_cast<ExplodedNode*>(N)->isSink()); 336f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek Impl.insert(N); 337f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek } 3381eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 339f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek ExplodedNodeSet() {} 3401eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 341c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu inline void Add(ExplodedNode* N) { 342c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu if (N && !static_cast<ExplodedNode*>(N)->isSink()) Impl.insert(N); 343f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek } 3441eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 345cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek ExplodedNodeSet& operator=(const ExplodedNodeSet &X) { 346cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek Impl = X.Impl; 347cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek return *this; 348cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek } 3491eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 350c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef ImplTy::iterator iterator; 351c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef ImplTy::const_iterator const_iterator; 352f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 353fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek unsigned size() const { return Impl.size(); } 354fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek bool empty() const { return Impl.empty(); } 355fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek 356fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek void clear() { Impl.clear(); } 357fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek void insert(const ExplodedNodeSet &S) { 358fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek if (empty()) 359fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek Impl = S.Impl; 360fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek else 361fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek Impl.insert(S.begin(), S.end()); 362fee96e043108b6e24e7d4c5464bf89ac970a7f81Ted Kremenek } 3631eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 364f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline iterator begin() { return Impl.begin(); } 365f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline iterator end() { return Impl.end(); } 3661eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 367f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline const_iterator begin() const { return Impl.begin(); } 368f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline const_iterator end() const { return Impl.end(); } 3691eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump}; 3701eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3714241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek} // end clang namespace 3724241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 3734a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek// GraphTraits 3744a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 3754a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremeneknamespace llvm { 376c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu template<> struct GraphTraits<clang::ExplodedNode*> { 377c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef clang::ExplodedNode NodeType; 378c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef NodeType::succ_iterator ChildIteratorType; 3794a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef llvm::df_iterator<NodeType*> nodes_iterator; 3801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3814a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline NodeType* getEntryNode(NodeType* N) { 3824a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N; 3834a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3841eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3854a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_begin(NodeType* N) { 3864a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_begin(); 3874a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3881eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3894a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_end(NodeType* N) { 3904a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_end(); 3914a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3934a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_begin(NodeType* N) { 3944a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_begin(N); 3954a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3961eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3974a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_end(NodeType* N) { 3984a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_end(N); 3994a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4004a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek }; 4011eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 402c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu template<> struct GraphTraits<const clang::ExplodedNode*> { 403c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef const clang::ExplodedNode NodeType; 404c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef NodeType::const_succ_iterator ChildIteratorType; 4054a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef llvm::df_iterator<NodeType*> nodes_iterator; 4061eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4074a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline NodeType* getEntryNode(NodeType* N) { 4084a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N; 4094a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4114a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_begin(NodeType* N) { 4124a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_begin(); 4134a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4141eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4154a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_end(NodeType* N) { 4164a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_end(); 4174a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4181eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4194a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_begin(NodeType* N) { 4204a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_begin(N); 4214a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4221eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4234a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_end(NodeType* N) { 4244a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_end(N); 4254a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4264a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek }; 4271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4284a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek} // end llvm namespace 4294a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4304241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#endif 431