RangeConstraintManager.cpp revision 9c378f705405d37f49795d5e915989de774fe11f
14502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==// 24502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 34502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// The LLVM Compiler Infrastructure 44502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 54502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// This file is distributed under the University of Illinois Open Source 64502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// License. See LICENSE.TXT for details. 74502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 84502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===// 94502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump// This file defines RangeConstraintManager, a class that tracks simple 114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// equality and inequality constraints on symbolic values of GRState. 124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===// 144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "SimpleConstraintManager.h" 169b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/GRState.h" 179b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/GRStateTrait.h" 189b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/TransferFuncs.h" 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/Debug.h" 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/FoldingSet.h" 214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/ImmutableSet.h" 224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/raw_ostream.h" 234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekusing namespace clang; 259ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenekusing namespace ento; 264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 27ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamnamespace { class ConstraintRange {}; } 289beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenekstatic int ConstraintRangeIndex = 0; 294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 309beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// A Range represents the closed range [from, to]. The caller must 319beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// guarantee that from <= to. Note that Range is immutable, so as not 329beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// to subvert RangeSet's immutability. 33b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremeneknamespace { 34ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass Range : public std::pair<const llvm::APSInt*, 35b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek const llvm::APSInt*> { 364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek Range(const llvm::APSInt &from, const llvm::APSInt &to) 389beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) { 394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert(from <= to); 404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool Includes(const llvm::APSInt &v) const { 429beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *first <= v && v <= *second; 434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const llvm::APSInt &From() const { 459beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *first; 464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const llvm::APSInt &To() const { 489beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *second; 494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 509beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const llvm::APSInt *getConcreteValue() const { 519beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return &From() == &To() ? &From() : NULL; 524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek void Profile(llvm::FoldingSetNodeID &ID) const { 559beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek ID.AddPointer(&From()); 569beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek ID.AddPointer(&To()); 574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 60b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek 61ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeTrait : public llvm::ImutContainerInfo<Range> { 62b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenekpublic: 63b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek // When comparing if one Range is less than another, we should compare 64e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek // the actual APSInt values instead of their pointers. This keeps the order 65e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek // consistent (instead of comparing by pointer values) and can potentially 66e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek // be used to speed up some of the operations in RangeSet. 67b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek static inline bool isLess(key_type_ref lhs, key_type_ref rhs) { 681eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) && 69b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek *lhs.second < *rhs.second); 70b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek } 71b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek}; 72b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek 739beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// RangeSet contains a set of ranges. If the set is empty, then 749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// there the value of a symbol is overly constrained and there are no 759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// possible values for that symbol. 76ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeSet { 77b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet; 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek PrimRangeSet ranges; // no need to make const, since it is an 794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // ImmutableSet - this allows default operator= 801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump // to work. 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 829beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek typedef PrimRangeSet::Factory Factory; 839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek typedef PrimRangeSet::iterator iterator; 844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 859beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek RangeSet(PrimRangeSet RS) : ranges(RS) {} 864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 879beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek iterator begin() const { return ranges.begin(); } 889beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek iterator end() const { return ranges.end(); } 891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek bool isEmpty() const { return ranges.isEmpty(); } 911eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 929beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// Construct a new RangeSet representing '{ [from, to] }'. 939beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to) 943baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek : ranges(F.add(F.getEmptySet(), Range(from, to))) {} 951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 969beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// Profile - Generates a hash profile of this RangeSet for use 979beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// by FoldingSet. 989beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); } 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// getConcreteValue - If a symbol is contrained to equal a specific integer 1019beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// constant then this method returns that value. Otherwise, it returns 1029beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// NULL. 1039beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const llvm::APSInt* getConcreteValue() const { 1049beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0; 1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 107ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseprivate: 108ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose void IntersectInRange(BasicValueFactory &BV, Factory &F, 109ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Lower, 110ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Upper, 111ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet &newRanges, 112ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet::iterator &i, 113ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet::iterator &e) const { 114ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // There are six cases for each range R in the set: 115ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 1. R is entirely before the intersection range. 116ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 2. R is entirely after the intersection range. 117ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 3. R contains the entire intersection range. 118ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 4. R starts before the intersection range and ends in the middle. 119ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 5. R starts in the middle of the intersection range and ends after it. 120ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 6. R is entirely contained in the intersection range. 121ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // These correspond to each of the conditions below. 122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose for (/* i = begin(), e = end() */; i != e; ++i) { 123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->To() < Lower) { 124ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose continue; 125ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 126ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->From() > Upper) { 1279beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek break; 1284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 130ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->Includes(Lower)) { 131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->Includes(Upper)) { 1323baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, Range(BV.getValue(Lower), 133ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BV.getValue(Upper))); 134ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } else 1363baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To())); 137ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } else { 138ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->Includes(Upper)) { 1393baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper))); 140ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 141ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } else 1423baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, *i); 143ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 1444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 147ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosepublic: 148ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Returns a set containing the values in the receiving set, intersected with 149ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // the closed range [Lower, Upper]. Unlike the Range type, this range uses 150ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // modular arithmetic, corresponding to the common treatment of C integer 151ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // overflow. Thus, if the Lower bound is greater than the Upper bound, the 152ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // range is taken to wrap around. This is equivalent to taking the 153ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // intersection with the two ranges [Min, Upper] and [Lower, Max], 154ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // or, alternatively, /removing/ all integers between Upper and Lower. 155ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet Intersect(BasicValueFactory &BV, Factory &F, 156ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Lower, 157ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Upper) const { 1583baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek PrimRangeSet newRanges = F.getEmptySet(); 1594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 160ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet::iterator i = begin(), e = end(); 161ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Lower <= Upper) 162ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, Lower, Upper, newRanges, i, e); 163ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose else { 164ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // The order of the next two statements is important! 165ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // IntersectInRange() does not reset the iteration state for i and e. 166ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Therefore, the lower range most be handled first. 167ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e); 168ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e); 1694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1709beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return newRanges; 1714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1735f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner void print(raw_ostream &os) const { 1749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek bool isFirst = true; 1754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << "{ "; 1769beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (iterator i = begin(), e = end(); i != e; ++i) { 1779beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek if (isFirst) 1789beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek isFirst = false; 1799beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek else 1804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << ", "; 1811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << '[' << i->From().toString(10) << ", " << i->To().toString(10) 1834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek << ']'; 1844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1851eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump os << " }"; 1869beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek } 1871eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool operator==(const RangeSet &other) const { 1894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return ranges == other.ranges; 1904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 192b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek} // end anonymous namespace 1934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1949beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenektypedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy; 1954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 1979ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenektemplate<> 1999beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenekstruct GRStateTrait<ConstraintRange> 2009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek : public GRStatePartialTrait<ConstraintRangeTy> { 2019c378f705405d37f49795d5e915989de774fe11fTed Kremenek static inline void *GDMIndex() { return &ConstraintRangeIndex; } 2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 2031eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump} 2045a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} 2051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace { 207ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeConstraintManager : public SimpleConstraintManager{ 2081eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump RangeSet GetRange(const GRState *state, SymbolRef sym); 2094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 210d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis RangeConstraintManager(SubEngine &subengine) 21132a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek : SimpleConstraintManager(subengine) {} 2124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2139c378f705405d37f49795d5e915989de774fe11fTed Kremenek const GRState *assumeSymNE(const GRState *state, SymbolRef sym, 214ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 215ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2179c378f705405d37f49795d5e915989de774fe11fTed Kremenek const GRState *assumeSymEQ(const GRState *state, SymbolRef sym, 218ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 219ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2219c378f705405d37f49795d5e915989de774fe11fTed Kremenek const GRState *assumeSymLT(const GRState *state, SymbolRef sym, 222ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 223ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2259c378f705405d37f49795d5e915989de774fe11fTed Kremenek const GRState *assumeSymGT(const GRState *state, SymbolRef sym, 226ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2299c378f705405d37f49795d5e915989de774fe11fTed Kremenek const GRState *assumeSymGE(const GRState *state, SymbolRef sym, 230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2324502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2339c378f705405d37f49795d5e915989de774fe11fTed Kremenek const GRState *assumeSymLE(const GRState *state, SymbolRef sym, 234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2379c378f705405d37f49795d5e915989de774fe11fTed Kremenek const llvm::APSInt* getSymVal(const GRState *St, SymbolRef sym) const; 2381eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2399beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek // FIXME: Refactor into SimpleConstraintManager? 2409c378f705405d37f49795d5e915989de774fe11fTed Kremenek bool isEqual(const GRState *St, SymbolRef sym, const llvm::APSInt& V) const { 2419beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const llvm::APSInt *i = getSymVal(St, sym); 2429beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return i ? *i == V : false; 2439beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek } 2444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2459c378f705405d37f49795d5e915989de774fe11fTed Kremenek const GRState *removeDeadBindings(const GRState *St, SymbolReaper& SymReaper); 2464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2479c378f705405d37f49795d5e915989de774fe11fTed Kremenek void print(const GRState *St, raw_ostream &Out, 2484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const char* nl, const char *sep); 2494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekprivate: 2519beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek RangeSet::Factory F; 2524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 2534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end anonymous namespace 2554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2569ef6537a894c33003359b1f9b9676e9178e028b7Ted KremenekConstraintManager* ento::CreateRangeConstraintManager(GRStateManager&, 257d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis SubEngine &subeng) { 25832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek return new RangeConstraintManager(subeng); 2594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2619c378f705405d37f49795d5e915989de774fe11fTed Kremenekconst llvm::APSInt* RangeConstraintManager::getSymVal(const GRState *St, 2624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym) const { 2639beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym); 2649beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return T ? T->getConcreteValue() : NULL; 2654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// Scan all symbols referenced by the constraints. If the symbol is not alive 2684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// as marked in LSymbols, mark it as dead in DSymbols. 2694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 2709c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::removeDeadBindings(const GRState *state, 2714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolReaper& SymReaper) { 2724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 273c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek ConstraintRangeTy CR = state->get<ConstraintRange>(); 274c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>(); 2754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2769beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { 2771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump SymbolRef sym = I.getKey(); 2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (SymReaper.maybeDead(sym)) 2793baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek CR = CRFactory.remove(CR, sym); 2804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 282c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek return state->set<ConstraintRange>(CR); 2839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek} 2849beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 2859beefec2a9f5d34ab70fef06515c7987cb041f07Ted KremenekRangeSet 286c87813824896a7124d2dd1c08e4661bbe119abf5Ted KremenekRangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) { 287c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym)) 2889beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *V; 2891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek // Lazily generate a new RangeSet representing all possible values for the 2919beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek // given symbol type. 292c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek QualType T = state->getSymbolManager().getType(sym); 2931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump BasicValueFactory& BV = state->getBasicVals(); 2949beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T)); 2954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2979beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------=== 29828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek// assumeSymX methods: public interface for RangeConstraintManager. 2999beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/ 3009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 301ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// The syntax for ranges below is mathematical, using [x, y] for closed ranges 302ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// and (x, y) for open ranges. These ranges are modular, corresponding with 303ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// a common treatment of C integer overflow. This means that these methods 304ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// do not have to worry about overflow; RangeSet::Intersect can handle such a 305ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// "wraparound" range. 306ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1, 307ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// UINT_MAX, 0, 1, and 2. 308ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 309ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState* 3109c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymNE(const GRState *state, SymbolRef sym, 311ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 312ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) { 313ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BasicValueFactory &BV = state->getBasicVals(); 314ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 315ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Int-Adjustment; 316ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Lower; 317ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose --Lower; 318ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose ++Upper; 319ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 320ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // [Int-Adjustment+1, Int-Adjustment-1] 321ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Notice that the lower bound is greater than the upper bound. 322ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower); 323ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); 3249beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek} 3259beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 326ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState* 3279c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymEQ(const GRState *state, SymbolRef sym, 328ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 329ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) { 330ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // [Int-Adjustment, Int-Adjustment] 331ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BasicValueFactory &BV = state->getBasicVals(); 332ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt AdjInt = Int-Adjustment; 333ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt); 334ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); 335ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 336ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 337ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState* 3389c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymLT(const GRState *state, SymbolRef sym, 339ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 340ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) { 341ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BasicValueFactory &BV = state->getBasicVals(); 342ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 343ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose QualType T = state->getSymbolManager().getType(sym); 344ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Min = BV.getMinValue(T); 345ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 346ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Min. This is always false. 347ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Int == Min) 348ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return NULL; 349ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 350ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Min-Adjustment; 351ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Int-Adjustment; 352ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose --Upper; 353ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 354ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); 355ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); 356ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 357ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 358ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState* 3599c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymGT(const GRState *state, SymbolRef sym, 360ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 361ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) { 362ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BasicValueFactory &BV = state->getBasicVals(); 363ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 364ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose QualType T = state->getSymbolManager().getType(sym); 365ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Max = BV.getMaxValue(T); 366ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 367ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Max. This is always false. 368ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Int == Max) 369ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return NULL; 370ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 371ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Int-Adjustment; 372ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Max-Adjustment; 373ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose ++Lower; 374ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 375ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); 376ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); 377ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 378ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 379ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState* 3809c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymGE(const GRState *state, SymbolRef sym, 381ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 382ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) { 383ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BasicValueFactory &BV = state->getBasicVals(); 384ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 385ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose QualType T = state->getSymbolManager().getType(sym); 386ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Min = BV.getMinValue(T); 387ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 388ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Min. This is always feasible. 389ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Int == Min) 390ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 391ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 392ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Max = BV.getMaxValue(T); 393ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 394ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Int-Adjustment; 395ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Max-Adjustment; 396ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 397ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); 398ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); 399ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 400ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 401ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState* 4029c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymLE(const GRState *state, SymbolRef sym, 403ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 404ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment) { 405ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BasicValueFactory &BV = state->getBasicVals(); 406ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 407ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose QualType T = state->getSymbolManager().getType(sym); 408ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Max = BV.getMaxValue(T); 409ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 410ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Max. This is always feasible. 411ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Int == Max) 412ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 413ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 414ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Min = BV.getMinValue(T); 415ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 416ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Min-Adjustment; 417ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Int-Adjustment; 418ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 419ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); 420ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); 421ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 4229beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 4239beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------=== 4249beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek// Pretty-printing. 4259beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/ 4269beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 4279c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid RangeConstraintManager::print(const GRState *St, raw_ostream &Out, 4284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const char* nl, const char *sep) { 4291eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4309beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek ConstraintRangeTy Ranges = St->get<ConstraintRange>(); 4311eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 432dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek if (Ranges.isEmpty()) 433dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek return; 4341eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 435dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek Out << nl << sep << "ranges of symbol values:"; 4361eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4379beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){ 438ec751c48bc904ec42bc3ce93a198b14a46dc8e01Ted Kremenek Out << nl << ' ' << I.getKey() << " : "; 43953ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek I.getData().print(Out); 4404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 4414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 442