ExplodedGraph.h revision 25e695b2d574d919cc1bbddf3a2efe073d449b1c
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." 124241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek// 134241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek//===----------------------------------------------------------------------===// 144241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 154241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#ifndef LLVM_CLANG_ANALYSIS_EXPLODEDGRAPH 164241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#define LLVM_CLANG_ANALYSIS_EXPLODEDGRAPH 174241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 184a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek#include "clang/Analysis/ProgramPoint.h" 1963bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek#include "clang/AST/Decl.h" 204241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#include "llvm/ADT/SmallVector.h" 214241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#include "llvm/ADT/FoldingSet.h" 22f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek#include "llvm/ADT/SmallPtrSet.h" 234241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#include "llvm/Support/Allocator.h" 24ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek#include "llvm/ADT/OwningPtr.h" 254a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek#include "llvm/ADT/GraphTraits.h" 264a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek#include "llvm/ADT/DepthFirstIterator.h" 2763bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek#include "llvm/Support/Casting.h" 284241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 294241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremeneknamespace clang { 304a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 31c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xuclass GRState; 3211062b118476368fa5b294954713e5df97d8599fTed Kremenekclass CFG; 3311062b118476368fa5b294954713e5df97d8599fTed Kremenekclass ASTContext; 3411062b118476368fa5b294954713e5df97d8599fTed Kremenek 35cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek//===----------------------------------------------------------------------===// 36cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek// ExplodedGraph "implementation" classes. These classes are not typed to 37cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek// contain a specific kind of state. Typed-specialized versions are defined 38cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek// on top of these classes. 39cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek//===----------------------------------------------------------------------===// 40cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek 41c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xuclass ExplodedNode : public llvm::FoldingSetNode { 4238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu friend class ExplodedGraph; 430111f575b968e423dccae439e501225b8314b257Zhongxing Xu friend class GRCoreEngine; 44031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRStmtNodeBuilder; 45031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRBranchNodeBuilder; 46031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRIndirectGotoNodeBuilder; 47031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GRSwitchNodeBuilder; 48031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu friend class GREndPathNodeBuilder; 494a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 504c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek class NodeGroup { 51b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek enum { Size1 = 0x0, SizeOther = 0x1, AuxFlag = 0x2, Mask = 0x3 }; 524c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek uintptr_t P; 534c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 54ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek unsigned getKind() const { 55596f0a1e54f610926e8bfded9efa1c639f824dedTed Kremenek return P & 0x1; 56ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek } 57ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek 58ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek void* getPtr() const { 59ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek assert (!getFlag()); 60b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek return reinterpret_cast<void*>(P & ~Mask); 61ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek } 62ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek 63c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode *getNode() const { 64c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu return reinterpret_cast<ExplodedNode*>(getPtr()); 65ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek } 664c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 674c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek public: 684c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek NodeGroup() : P(0) {} 694c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 709eb49a40df510313132eef147419c5abefff23ebTed Kremenek ~NodeGroup(); 714c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 72c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode** begin() const; 734c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 74c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode** end() const; 754c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 765d5480380d7b7c3590a0283ddf239220e514e576Ted Kremenek unsigned size() const; 774c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 78ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek bool empty() const { return size() == 0; } 794c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 80c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu void addNode(ExplodedNode* N); 81f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek 82b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek void setFlag() { 83ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek assert (P == 0); 84ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek P = AuxFlag; 85f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek } 86f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek 87b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek bool getFlag() const { 88b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek return P & AuxFlag ? true : false; 89f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek } 90b38911f16b4943548db6a3695fc6ae23070b25d2Ted Kremenek }; 914c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek 924a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// Location - The program location (within a function body) associated 934a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// with this node. 944a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const ProgramPoint Location; 954a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 964323a57627e796dcfdfdb7d47672dc09ed308edaTed Kremenek /// State - The state associated with this node. 97c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu const GRState* State; 984a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 994a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// Preds - The predecessors of this node. 1004c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek NodeGroup Preds; 1014a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 1024a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// Succs - The successors of this node. 1034c4cb527a44037d076da82ad9d12b4e655e64dbbTed Kremenek NodeGroup Succs; 104c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1054a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenekpublic: 106c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 107c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu explicit ExplodedNode(const ProgramPoint& loc, const GRState* state) 108c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu : Location(loc), State(state) {} 109c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1104a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek /// getLocation - Returns the edge associated with the given node. 1110f9063c116b7c3b05d8042b5976463c2dae04861Ted Kremenek ProgramPoint getLocation() const { return Location; } 112c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 11325e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu const LocationContext *getLocationContext() const { 11425e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu return getLocation().getContext(); 11525e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu } 11625e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu 117c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu const GRState* getState() const { 118c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu return State; 119c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu } 120c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 12152c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek template <typename T> 12252c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek const T* getLocationAs() const { return llvm::dyn_cast<T>(&Location); } 123c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 124c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu static void Profile(llvm::FoldingSetNodeID &ID, 125c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu const ProgramPoint& Loc, const GRState* state); 126c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 127c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu void Profile(llvm::FoldingSetNodeID& ID) const { 128c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu Profile(ID, getLocation(), getState()); 129c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu } 130c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 131c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu /// addPredeccessor - Adds a predecessor to the current node, and 132c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu /// in tandem add this node as a successor of the other node. 133c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu void addPredecessor(ExplodedNode* V); 134c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 1354a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek unsigned succ_size() const { return Succs.size(); } 1364a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek unsigned pred_size() const { return Preds.size(); } 1374a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek bool succ_empty() const { return Succs.empty(); } 1380e8a3c743b9b3e3039e329a1736122d3b5b5fed9Ted Kremenek bool pred_empty() const { return Preds.empty(); } 139f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek 140ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek bool isSink() const { return Succs.getFlag(); } 1412e287540c90255e14208e7e5f43f07cb752a1fd7Ted Kremenek void markAsSink() { Succs.setFlag(); } 1424a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 14352c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek ExplodedNode* getFirstPred() { 14452c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek return pred_empty() ? NULL : *(pred_begin()); 14552c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek } 14652c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek 14752c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek const ExplodedNode* getFirstPred() const { 14852c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek return const_cast<ExplodedNode*>(this)->getFirstPred(); 14952c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek } 15052c3196a89a26cebcf069dd140c3396b743b8e33Ted Kremenek 1514a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek // Iterators over successor and predecessor vertices. 1524a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef ExplodedNode** succ_iterator; 1533148eb4a75f70f2636075c364d03104223f004d3Ted Kremenek typedef const ExplodedNode* const * const_succ_iterator; 1544a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef ExplodedNode** pred_iterator; 1553148eb4a75f70f2636075c364d03104223f004d3Ted Kremenek typedef const ExplodedNode* const * const_pred_iterator; 1564a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 157c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu pred_iterator pred_begin() { return Preds.begin(); } 158c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu pred_iterator pred_end() { return Preds.end(); } 1594a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 1604a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_pred_iterator pred_begin() const { 1614a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->pred_begin(); 1624a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 1634a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_pred_iterator pred_end() const { 1644a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->pred_end(); 1654a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 1664a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 167c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu succ_iterator succ_begin() { return Succs.begin(); } 168c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu succ_iterator succ_end() { return Succs.end(); } 1694a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 1704a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_succ_iterator succ_begin() const { 1714a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->succ_begin(); 1724a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 1734a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek const_succ_iterator succ_end() const { 1744a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return const_cast<ExplodedNode*>(this)->succ_end(); 1754a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 176c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 177c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu // For debugging. 178c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 179c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xupublic: 180c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 181c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu class Auditor { 182c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu public: 183c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu virtual ~Auditor(); 184c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu virtual void AddEdge(ExplodedNode* Src, ExplodedNode* Dst) = 0; 185c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu }; 186c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 187c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu static void SetAuditor(Auditor* A); 188c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu}; 189c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 19038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu// FIXME: Is this class necessary? 19138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xuclass InterExplodedGraphMap { 19238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::DenseMap<const ExplodedNode*, ExplodedNode*> M; 19338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu friend class ExplodedGraph; 194c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 19538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xupublic: 19638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedNode* getMappedNode(const ExplodedNode* N) const; 19738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 19838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu InterExplodedGraphMap() {}; 19938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu virtual ~InterExplodedGraphMap() {} 2004a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek}; 2014a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 20238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xuclass ExplodedGraph { 2034241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenekprotected: 2040111f575b968e423dccae439e501225b8314b257Zhongxing Xu friend class GRCoreEngine; 205e96de2dfde487211fb52f9139cdcae64d051a406Zhongxing Xu 2064241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek // Type definitions. 207c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef llvm::SmallVector<ExplodedNode*,2> RootsTy; 208c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef llvm::SmallVector<ExplodedNode*,10> EndNodesTy; 209ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek 2104241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// Roots - The roots of the simulation graph. Usually there will be only 2114241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// one, but clients are free to establish multiple subgraphs within a single 2124241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// SimulGraph. Moreover, these subgraphs can often merge when paths from 2134241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// different roots reach the same state at the same program location. 2144241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek RootsTy Roots; 2154241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 2164241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// EndNodes - The nodes in the simulation graph which have been 2174241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// specially marked as the endpoint of an abstract simulation path. 2184241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek EndNodesTy EndNodes; 21938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 22038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// Nodes - The nodes in the graph. 22138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::FoldingSet<ExplodedNode> Nodes; 22238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 2234241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// Allocator - BumpPtrAllocator to create nodes. 2244241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek llvm::BumpPtrAllocator Allocator; 225cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek 226cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek /// cfg - The CFG associated with this analysis graph. 227cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek CFG& cfg; 228cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek 22963bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek /// CodeDecl - The declaration containing the code being analyzed. This 23063bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek /// can be a FunctionDecl or and ObjCMethodDecl. 23163bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek Decl& CodeDecl; 232cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek 23363bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek /// Ctx - The ASTContext used to "interpret" CodeDecl. 234cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek ASTContext& Ctx; 23539b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek 23639b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek /// NumNodes - The number of nodes in the graph. 23739b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek unsigned NumNodes; 2384241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 23938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xupublic: 24038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// getNode - Retrieve the node associated with a (Location,State) pair, 24138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// where the 'Location' is a ProgramPoint in the CFG. If no node for 24238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// this pair exists, it is created. IsNew is set to true if 24338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu /// the node was freshly created. 24438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 24538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedNode* getNode(const ProgramPoint& L, const GRState *State, 24638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu bool* IsNew = 0); 247ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek 24838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedGraph* MakeEmptyGraph() const { 24938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu return new ExplodedGraph(cfg, CodeDecl, Ctx); 25038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu } 2514a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 2524241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// addRoot - Add an untyped node to the set of roots. 253c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode* addRoot(ExplodedNode* V) { 254ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek Roots.push_back(V); 255ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek return V; 256ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek } 2574241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 2584241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek /// addEndOfPath - Add an untyped node to the set of EOP nodes. 259c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNode* addEndOfPath(ExplodedNode* V) { 260ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek EndNodes.push_back(V); 261ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek return V; 262ede5a4ba111f0590879670b6cb07f4d6d0bd9075Ted Kremenek } 26338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 26438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedGraph(CFG& c, Decl& cd, ASTContext& ctx) 26563bbe5312cd89ce0ceb684bff68c5baef636e93cTed Kremenek : cfg(c), CodeDecl(cd), Ctx(ctx), NumNodes(0) {} 2664241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 26738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu virtual ~ExplodedGraph() {} 2684a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 2694241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek unsigned num_roots() const { return Roots.size(); } 2704a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek unsigned num_eops() const { return EndNodes.size(); } 271cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek 27239b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek bool empty() const { return NumNodes == 0; } 27339b4c6c98d391b25c376782cf92346aa88c96f7eTed Kremenek unsigned size() const { return NumNodes; } 274c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu 2754241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek // Iterators. 27638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef ExplodedNode NodeTy; 27738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef llvm::FoldingSet<ExplodedNode> AllNodesTy; 2787ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek typedef NodeTy** roots_iterator; 27938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef NodeTy* const * const_roots_iterator; 2807ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek typedef NodeTy** eop_iterator; 28138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef NodeTy* const * const_eop_iterator; 28238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef AllNodesTy::iterator node_iterator; 28338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef AllNodesTy::const_iterator const_node_iterator; 2847ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek 28538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu node_iterator nodes_begin() { return Nodes.begin(); } 2867ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek 28738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu node_iterator nodes_end() { return Nodes.end(); } 2884241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 28938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_node_iterator nodes_begin() const { return Nodes.begin(); } 2907ebde953bb050caa69f791fc1de449d435c6a36fTed Kremenek 29138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_node_iterator nodes_end() const { return Nodes.end(); } 2924241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 29338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu roots_iterator roots_begin() { return Roots.begin(); } 2944241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 29538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu roots_iterator roots_end() { return Roots.end(); } 2964241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 29738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_roots_iterator roots_begin() const { return Roots.begin(); } 2984241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 29938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_roots_iterator roots_end() const { return Roots.end(); } 3004241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 30138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu eop_iterator eop_begin() { return EndNodes.begin(); } 3024241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 30338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu eop_iterator eop_end() { return EndNodes.end(); } 3044241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 30538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_eop_iterator eop_begin() const { return EndNodes.begin(); } 3064241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 30738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const_eop_iterator eop_end() const { return EndNodes.end(); } 30838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 30938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::BumpPtrAllocator& getAllocator() { return Allocator; } 31038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu CFG& getCFG() { return cfg; } 31138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ASTContext& getContext() { return Ctx; } 31238b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 31338b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu Decl& getCodeDecl() { return CodeDecl; } 31438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const Decl& getCodeDecl() const { return CodeDecl; } 31538b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 31638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const FunctionDecl* getFunctionDecl() const { 31738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu return llvm::dyn_cast<FunctionDecl>(&CodeDecl); 3184241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek } 319ffe0f43806d4823271c2406c1fccc2373115c36aTed Kremenek 32038b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu typedef llvm::DenseMap<const ExplodedNode*, ExplodedNode*> NodeMap; 32138b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu 322c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu std::pair<ExplodedGraph*, InterExplodedGraphMap*> 323fe9e543a2a363df7fcaa899367d3b2580b63b27cTed Kremenek Trim(const NodeTy* const* NBeg, const NodeTy* const* NEnd, 32438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::DenseMap<const void*, const void*> *InverseMap = 0) const; 325cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek 32638b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu ExplodedGraph* TrimInternal(const ExplodedNode* const * NBeg, 32738b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu const ExplodedNode* const * NEnd, 32838b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu InterExplodedGraphMap *M, 32938b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::DenseMap<const void*, const void*> *InverseMap) const; 3304241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek}; 331cf118d41f7930a18dce97416ef7834a62642f587Ted Kremenek 332f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenekclass ExplodedNodeSet { 333c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef llvm::SmallPtrSet<ExplodedNode*,5> ImplTy; 334f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek ImplTy Impl; 335f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 336f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenekpublic: 337c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu ExplodedNodeSet(ExplodedNode* N) { 338c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu assert (N && !static_cast<ExplodedNode*>(N)->isSink()); 339f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek Impl.insert(N); 340f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek } 341f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 342f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek ExplodedNodeSet() {} 343f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 344c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu inline void Add(ExplodedNode* N) { 345c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu if (N && !static_cast<ExplodedNode*>(N)->isSink()) Impl.insert(N); 346f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek } 347f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 348cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek ExplodedNodeSet& operator=(const ExplodedNodeSet &X) { 349cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek Impl = X.Impl; 350cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek return *this; 351cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek } 352cc2c6eb04d882466c7cfbb544c251d7e0ba0f356Ted Kremenek 353c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef ImplTy::iterator iterator; 354c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef ImplTy::const_iterator const_iterator; 355f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 356f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline unsigned size() const { return Impl.size(); } 357f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline bool empty() const { return Impl.empty(); } 3584bf38da038cebf9396470630c3c39519e41706daTed Kremenek 3594bf38da038cebf9396470630c3c39519e41706daTed Kremenek inline void clear() { Impl.clear(); } 360f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 361f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline iterator begin() { return Impl.begin(); } 362f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline iterator end() { return Impl.end(); } 363f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 364f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline const_iterator begin() const { return Impl.begin(); } 365f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek inline const_iterator end() const { return Impl.end(); } 366f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek}; 367f6f5ef4aaa66b60270e84d1fe1292886369d2f38Ted Kremenek 3684241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek} // end clang namespace 3694241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek 3704a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek// GraphTraits 3714a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 3724a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremeneknamespace llvm { 373c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu template<> struct GraphTraits<clang::ExplodedNode*> { 374c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef clang::ExplodedNode NodeType; 375c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef NodeType::succ_iterator ChildIteratorType; 3764a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef llvm::df_iterator<NodeType*> nodes_iterator; 3774a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 3784a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline NodeType* getEntryNode(NodeType* N) { 3794a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N; 3804a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3814a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 3824a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_begin(NodeType* N) { 3834a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_begin(); 3844a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3854a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 3864a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_end(NodeType* N) { 3874a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_end(); 3884a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3894a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 3904a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_begin(NodeType* N) { 3914a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_begin(N); 3924a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3934a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 3944a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_end(NodeType* N) { 3954a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_end(N); 3964a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 3974a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek }; 3984a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 399c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu template<> struct GraphTraits<const clang::ExplodedNode*> { 400c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef const clang::ExplodedNode NodeType; 401c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing Xu typedef NodeType::const_succ_iterator ChildIteratorType; 4024a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek typedef llvm::df_iterator<NodeType*> nodes_iterator; 4034a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4044a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline NodeType* getEntryNode(NodeType* N) { 4054a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N; 4064a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4074a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4084a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_begin(NodeType* N) { 4094a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_begin(); 4104a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4114a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4124a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline ChildIteratorType child_end(NodeType* N) { 4134a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return N->succ_end(); 4144a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4154a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4164a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_begin(NodeType* N) { 4174a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_begin(N); 4184a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4194a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4204a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek static inline nodes_iterator nodes_end(NodeType* N) { 4214a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek return df_end(N); 4224a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek } 4234a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek }; 4244a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4254a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek} // end llvm namespace 4264a0f5f1646637fcf90eb236b5a46f40e5a5dd739Ted Kremenek 4274241b3d1ad87e9a593bbc6cdf0f49435d5aec235Ted Kremenek#endif 428