clang API Documentation

RangeConstraintManager.cpp
Go to the documentation of this file.
00001 //== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
00002 //
00003 //                     The LLVM Compiler Infrastructure
00004 //
00005 // This file is distributed under the University of Illinois Open Source
00006 // License. See LICENSE.TXT for details.
00007 //
00008 //===----------------------------------------------------------------------===//
00009 //
00010 //  This file defines RangeConstraintManager, a class that tracks simple
00011 //  equality and inequality constraints on symbolic values of ProgramState.
00012 //
00013 //===----------------------------------------------------------------------===//
00014 
00015 #include "SimpleConstraintManager.h"
00016 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
00017 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
00018 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
00019 #include "llvm/ADT/FoldingSet.h"
00020 #include "llvm/ADT/ImmutableSet.h"
00021 #include "llvm/Support/Debug.h"
00022 #include "llvm/Support/raw_ostream.h"
00023 
00024 using namespace clang;
00025 using namespace ento;
00026 
00027 /// A Range represents the closed range [from, to].  The caller must
00028 /// guarantee that from <= to.  Note that Range is immutable, so as not
00029 /// to subvert RangeSet's immutability.
00030 namespace {
00031 class Range : public std::pair<const llvm::APSInt*,
00032                                                 const llvm::APSInt*> {
00033 public:
00034   Range(const llvm::APSInt &from, const llvm::APSInt &to)
00035     : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
00036     assert(from <= to);
00037   }
00038   bool Includes(const llvm::APSInt &v) const {
00039     return *first <= v && v <= *second;
00040   }
00041   const llvm::APSInt &From() const {
00042     return *first;
00043   }
00044   const llvm::APSInt &To() const {
00045     return *second;
00046   }
00047   const llvm::APSInt *getConcreteValue() const {
00048     return &From() == &To() ? &From() : nullptr;
00049   }
00050 
00051   void Profile(llvm::FoldingSetNodeID &ID) const {
00052     ID.AddPointer(&From());
00053     ID.AddPointer(&To());
00054   }
00055 };
00056 
00057 
00058 class RangeTrait : public llvm::ImutContainerInfo<Range> {
00059 public:
00060   // When comparing if one Range is less than another, we should compare
00061   // the actual APSInt values instead of their pointers.  This keeps the order
00062   // consistent (instead of comparing by pointer values) and can potentially
00063   // be used to speed up some of the operations in RangeSet.
00064   static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
00065     return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
00066                                        *lhs.second < *rhs.second);
00067   }
00068 };
00069 
00070 /// RangeSet contains a set of ranges. If the set is empty, then
00071 ///  there the value of a symbol is overly constrained and there are no
00072 ///  possible values for that symbol.
00073 class RangeSet {
00074   typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
00075   PrimRangeSet ranges; // no need to make const, since it is an
00076                        // ImmutableSet - this allows default operator=
00077                        // to work.
00078 public:
00079   typedef PrimRangeSet::Factory Factory;
00080   typedef PrimRangeSet::iterator iterator;
00081 
00082   RangeSet(PrimRangeSet RS) : ranges(RS) {}
00083 
00084   iterator begin() const { return ranges.begin(); }
00085   iterator end() const { return ranges.end(); }
00086 
00087   bool isEmpty() const { return ranges.isEmpty(); }
00088 
00089   /// Construct a new RangeSet representing '{ [from, to] }'.
00090   RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
00091     : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
00092 
00093   /// Profile - Generates a hash profile of this RangeSet for use
00094   ///  by FoldingSet.
00095   void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
00096 
00097   /// getConcreteValue - If a symbol is contrained to equal a specific integer
00098   ///  constant then this method returns that value.  Otherwise, it returns
00099   ///  NULL.
00100   const llvm::APSInt* getConcreteValue() const {
00101     return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
00102   }
00103 
00104 private:
00105   void IntersectInRange(BasicValueFactory &BV, Factory &F,
00106                         const llvm::APSInt &Lower,
00107                         const llvm::APSInt &Upper,
00108                         PrimRangeSet &newRanges,
00109                         PrimRangeSet::iterator &i,
00110                         PrimRangeSet::iterator &e) const {
00111     // There are six cases for each range R in the set:
00112     //   1. R is entirely before the intersection range.
00113     //   2. R is entirely after the intersection range.
00114     //   3. R contains the entire intersection range.
00115     //   4. R starts before the intersection range and ends in the middle.
00116     //   5. R starts in the middle of the intersection range and ends after it.
00117     //   6. R is entirely contained in the intersection range.
00118     // These correspond to each of the conditions below.
00119     for (/* i = begin(), e = end() */; i != e; ++i) {
00120       if (i->To() < Lower) {
00121         continue;
00122       }
00123       if (i->From() > Upper) {
00124         break;
00125       }
00126 
00127       if (i->Includes(Lower)) {
00128         if (i->Includes(Upper)) {
00129           newRanges = F.add(newRanges, Range(BV.getValue(Lower),
00130                                              BV.getValue(Upper)));
00131           break;
00132         } else
00133           newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
00134       } else {
00135         if (i->Includes(Upper)) {
00136           newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
00137           break;
00138         } else
00139           newRanges = F.add(newRanges, *i);
00140       }
00141     }
00142   }
00143 
00144   const llvm::APSInt &getMinValue() const {
00145     assert(!isEmpty());
00146     return ranges.begin()->From();
00147   }
00148 
00149   bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
00150     // This function has nine cases, the cartesian product of range-testing
00151     // both the upper and lower bounds against the symbol's type.
00152     // Each case requires a different pinning operation.
00153     // The function returns false if the described range is entirely outside
00154     // the range of values for the associated symbol.
00155     APSIntType Type(getMinValue());
00156     APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true);
00157     APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true);
00158 
00159     switch (LowerTest) {
00160     case APSIntType::RTR_Below:
00161       switch (UpperTest) {
00162       case APSIntType::RTR_Below:
00163         // The entire range is outside the symbol's set of possible values.
00164         // If this is a conventionally-ordered range, the state is infeasible.
00165         if (Lower < Upper)
00166           return false;
00167 
00168         // However, if the range wraps around, it spans all possible values.
00169         Lower = Type.getMinValue();
00170         Upper = Type.getMaxValue();
00171         break;
00172       case APSIntType::RTR_Within:
00173         // The range starts below what's possible but ends within it. Pin.
00174         Lower = Type.getMinValue();
00175         Type.apply(Upper);
00176         break;
00177       case APSIntType::RTR_Above:
00178         // The range spans all possible values for the symbol. Pin.
00179         Lower = Type.getMinValue();
00180         Upper = Type.getMaxValue();
00181         break;
00182       }
00183       break;
00184     case APSIntType::RTR_Within:
00185       switch (UpperTest) {
00186       case APSIntType::RTR_Below:
00187         // The range wraps around, but all lower values are not possible.
00188         Type.apply(Lower);
00189         Upper = Type.getMaxValue();
00190         break;
00191       case APSIntType::RTR_Within:
00192         // The range may or may not wrap around, but both limits are valid.
00193         Type.apply(Lower);
00194         Type.apply(Upper);
00195         break;
00196       case APSIntType::RTR_Above:
00197         // The range starts within what's possible but ends above it. Pin.
00198         Type.apply(Lower);
00199         Upper = Type.getMaxValue();
00200         break;
00201       }
00202       break;
00203     case APSIntType::RTR_Above:
00204       switch (UpperTest) {
00205       case APSIntType::RTR_Below:
00206         // The range wraps but is outside the symbol's set of possible values.
00207         return false;
00208       case APSIntType::RTR_Within:
00209         // The range starts above what's possible but ends within it (wrap).
00210         Lower = Type.getMinValue();
00211         Type.apply(Upper);
00212         break;
00213       case APSIntType::RTR_Above:
00214         // The entire range is outside the symbol's set of possible values.
00215         // If this is a conventionally-ordered range, the state is infeasible.
00216         if (Lower < Upper)
00217           return false;
00218 
00219         // However, if the range wraps around, it spans all possible values.
00220         Lower = Type.getMinValue();
00221         Upper = Type.getMaxValue();
00222         break;
00223       }
00224       break;
00225     }
00226 
00227     return true;
00228   }
00229 
00230 public:
00231   // Returns a set containing the values in the receiving set, intersected with
00232   // the closed range [Lower, Upper]. Unlike the Range type, this range uses
00233   // modular arithmetic, corresponding to the common treatment of C integer
00234   // overflow. Thus, if the Lower bound is greater than the Upper bound, the
00235   // range is taken to wrap around. This is equivalent to taking the
00236   // intersection with the two ranges [Min, Upper] and [Lower, Max],
00237   // or, alternatively, /removing/ all integers between Upper and Lower.
00238   RangeSet Intersect(BasicValueFactory &BV, Factory &F,
00239                      llvm::APSInt Lower, llvm::APSInt Upper) const {
00240     if (!pin(Lower, Upper))
00241       return F.getEmptySet();
00242 
00243     PrimRangeSet newRanges = F.getEmptySet();
00244 
00245     PrimRangeSet::iterator i = begin(), e = end();
00246     if (Lower <= Upper)
00247       IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
00248     else {
00249       // The order of the next two statements is important!
00250       // IntersectInRange() does not reset the iteration state for i and e.
00251       // Therefore, the lower range most be handled first.
00252       IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
00253       IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
00254     }
00255 
00256     return newRanges;
00257   }
00258 
00259   void print(raw_ostream &os) const {
00260     bool isFirst = true;
00261     os << "{ ";
00262     for (iterator i = begin(), e = end(); i != e; ++i) {
00263       if (isFirst)
00264         isFirst = false;
00265       else
00266         os << ", ";
00267 
00268       os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
00269          << ']';
00270     }
00271     os << " }";
00272   }
00273 
00274   bool operator==(const RangeSet &other) const {
00275     return ranges == other.ranges;
00276   }
00277 };
00278 } // end anonymous namespace
00279 
00280 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange,
00281                                  CLANG_ENTO_PROGRAMSTATE_MAP(SymbolRef,
00282                                                              RangeSet))
00283 
00284 namespace {
00285 class RangeConstraintManager : public SimpleConstraintManager{
00286   RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
00287 public:
00288   RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB)
00289     : SimpleConstraintManager(subengine, SVB) {}
00290 
00291   ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
00292                              const llvm::APSInt& Int,
00293                              const llvm::APSInt& Adjustment) override;
00294 
00295   ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
00296                              const llvm::APSInt& Int,
00297                              const llvm::APSInt& Adjustment) override;
00298 
00299   ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
00300                              const llvm::APSInt& Int,
00301                              const llvm::APSInt& Adjustment) override;
00302 
00303   ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
00304                              const llvm::APSInt& Int,
00305                              const llvm::APSInt& Adjustment) override;
00306 
00307   ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
00308                              const llvm::APSInt& Int,
00309                              const llvm::APSInt& Adjustment) override;
00310 
00311   ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
00312                              const llvm::APSInt& Int,
00313                              const llvm::APSInt& Adjustment) override;
00314 
00315   const llvm::APSInt* getSymVal(ProgramStateRef St,
00316                                 SymbolRef sym) const override;
00317   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
00318 
00319   ProgramStateRef removeDeadBindings(ProgramStateRef St,
00320                                      SymbolReaper& SymReaper) override;
00321 
00322   void print(ProgramStateRef St, raw_ostream &Out,
00323              const char* nl, const char *sep) override;
00324 
00325 private:
00326   RangeSet::Factory F;
00327 };
00328 
00329 } // end anonymous namespace
00330 
00331 std::unique_ptr<ConstraintManager>
00332 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
00333   return llvm::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
00334 }
00335 
00336 const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
00337                                                       SymbolRef sym) const {
00338   const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
00339   return T ? T->getConcreteValue() : nullptr;
00340 }
00341 
00342 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
00343                                                     SymbolRef Sym) {
00344   const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
00345 
00346   // If we don't have any information about this symbol, it's underconstrained.
00347   if (!Ranges)
00348     return ConditionTruthVal();
00349 
00350   // If we have a concrete value, see if it's zero.
00351   if (const llvm::APSInt *Value = Ranges->getConcreteValue())
00352     return *Value == 0;
00353 
00354   BasicValueFactory &BV = getBasicVals();
00355   APSIntType IntType = BV.getAPSIntType(Sym->getType());
00356   llvm::APSInt Zero = IntType.getZeroValue();
00357 
00358   // Check if zero is in the set of possible values.
00359   if (Ranges->Intersect(BV, F, Zero, Zero).isEmpty())
00360     return false;
00361 
00362   // Zero is a possible value, but it is not the /only/ possible value.
00363   return ConditionTruthVal();
00364 }
00365 
00366 /// Scan all symbols referenced by the constraints. If the symbol is not alive
00367 /// as marked in LSymbols, mark it as dead in DSymbols.
00368 ProgramStateRef 
00369 RangeConstraintManager::removeDeadBindings(ProgramStateRef state,
00370                                            SymbolReaper& SymReaper) {
00371 
00372   ConstraintRangeTy CR = state->get<ConstraintRange>();
00373   ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
00374 
00375   for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
00376     SymbolRef sym = I.getKey();
00377     if (SymReaper.maybeDead(sym))
00378       CR = CRFactory.remove(CR, sym);
00379   }
00380 
00381   return state->set<ConstraintRange>(CR);
00382 }
00383 
00384 RangeSet
00385 RangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
00386   if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
00387     return *V;
00388 
00389   // Lazily generate a new RangeSet representing all possible values for the
00390   // given symbol type.
00391   BasicValueFactory &BV = getBasicVals();
00392   QualType T = sym->getType();
00393 
00394   RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
00395 
00396   // Special case: references are known to be non-zero.
00397   if (T->isReferenceType()) {
00398     APSIntType IntType = BV.getAPSIntType(T);
00399     Result = Result.Intersect(BV, F, ++IntType.getZeroValue(),
00400                                      --IntType.getZeroValue());
00401   }
00402 
00403   return Result;
00404 }
00405 
00406 //===------------------------------------------------------------------------===
00407 // assumeSymX methods: public interface for RangeConstraintManager.
00408 //===------------------------------------------------------------------------===/
00409 
00410 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
00411 // and (x, y) for open ranges. These ranges are modular, corresponding with
00412 // a common treatment of C integer overflow. This means that these methods
00413 // do not have to worry about overflow; RangeSet::Intersect can handle such a
00414 // "wraparound" range.
00415 // As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
00416 // UINT_MAX, 0, 1, and 2.
00417 
00418 ProgramStateRef 
00419 RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
00420                                     const llvm::APSInt &Int,
00421                                     const llvm::APSInt &Adjustment) {
00422   // Before we do any real work, see if the value can even show up.
00423   APSIntType AdjustmentType(Adjustment);
00424   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
00425     return St;
00426 
00427   llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
00428   llvm::APSInt Upper = Lower;
00429   --Lower;
00430   ++Upper;
00431 
00432   // [Int-Adjustment+1, Int-Adjustment-1]
00433   // Notice that the lower bound is greater than the upper bound.
00434   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
00435   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00436 }
00437 
00438 ProgramStateRef 
00439 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
00440                                     const llvm::APSInt &Int,
00441                                     const llvm::APSInt &Adjustment) {
00442   // Before we do any real work, see if the value can even show up.
00443   APSIntType AdjustmentType(Adjustment);
00444   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
00445     return nullptr;
00446 
00447   // [Int-Adjustment, Int-Adjustment]
00448   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
00449   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
00450   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00451 }
00452 
00453 ProgramStateRef 
00454 RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
00455                                     const llvm::APSInt &Int,
00456                                     const llvm::APSInt &Adjustment) {
00457   // Before we do any real work, see if the value can even show up.
00458   APSIntType AdjustmentType(Adjustment);
00459   switch (AdjustmentType.testInRange(Int, true)) {
00460   case APSIntType::RTR_Below:
00461     return nullptr;
00462   case APSIntType::RTR_Within:
00463     break;
00464   case APSIntType::RTR_Above:
00465     return St;
00466   }
00467 
00468   // Special case for Int == Min. This is always false.
00469   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00470   llvm::APSInt Min = AdjustmentType.getMinValue();
00471   if (ComparisonVal == Min)
00472     return nullptr;
00473 
00474   llvm::APSInt Lower = Min-Adjustment;
00475   llvm::APSInt Upper = ComparisonVal-Adjustment;
00476   --Upper;
00477 
00478   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00479   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00480 }
00481 
00482 ProgramStateRef 
00483 RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
00484                                     const llvm::APSInt &Int,
00485                                     const llvm::APSInt &Adjustment) {
00486   // Before we do any real work, see if the value can even show up.
00487   APSIntType AdjustmentType(Adjustment);
00488   switch (AdjustmentType.testInRange(Int, true)) {
00489   case APSIntType::RTR_Below:
00490     return St;
00491   case APSIntType::RTR_Within:
00492     break;
00493   case APSIntType::RTR_Above:
00494     return nullptr;
00495   }
00496 
00497   // Special case for Int == Max. This is always false.
00498   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00499   llvm::APSInt Max = AdjustmentType.getMaxValue();
00500   if (ComparisonVal == Max)
00501     return nullptr;
00502 
00503   llvm::APSInt Lower = ComparisonVal-Adjustment;
00504   llvm::APSInt Upper = Max-Adjustment;
00505   ++Lower;
00506 
00507   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00508   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00509 }
00510 
00511 ProgramStateRef 
00512 RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
00513                                     const llvm::APSInt &Int,
00514                                     const llvm::APSInt &Adjustment) {
00515   // Before we do any real work, see if the value can even show up.
00516   APSIntType AdjustmentType(Adjustment);
00517   switch (AdjustmentType.testInRange(Int, true)) {
00518   case APSIntType::RTR_Below:
00519     return St;
00520   case APSIntType::RTR_Within:
00521     break;
00522   case APSIntType::RTR_Above:
00523     return nullptr;
00524   }
00525 
00526   // Special case for Int == Min. This is always feasible.
00527   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00528   llvm::APSInt Min = AdjustmentType.getMinValue();
00529   if (ComparisonVal == Min)
00530     return St;
00531 
00532   llvm::APSInt Max = AdjustmentType.getMaxValue();
00533   llvm::APSInt Lower = ComparisonVal-Adjustment;
00534   llvm::APSInt Upper = Max-Adjustment;
00535 
00536   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00537   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00538 }
00539 
00540 ProgramStateRef 
00541 RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
00542                                     const llvm::APSInt &Int,
00543                                     const llvm::APSInt &Adjustment) {
00544   // Before we do any real work, see if the value can even show up.
00545   APSIntType AdjustmentType(Adjustment);
00546   switch (AdjustmentType.testInRange(Int, true)) {
00547   case APSIntType::RTR_Below:
00548     return nullptr;
00549   case APSIntType::RTR_Within:
00550     break;
00551   case APSIntType::RTR_Above:
00552     return St;
00553   }
00554 
00555   // Special case for Int == Max. This is always feasible.
00556   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00557   llvm::APSInt Max = AdjustmentType.getMaxValue();
00558   if (ComparisonVal == Max)
00559     return St;
00560 
00561   llvm::APSInt Min = AdjustmentType.getMinValue();
00562   llvm::APSInt Lower = Min-Adjustment;
00563   llvm::APSInt Upper = ComparisonVal-Adjustment;
00564 
00565   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00566   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00567 }
00568 
00569 //===------------------------------------------------------------------------===
00570 // Pretty-printing.
00571 //===------------------------------------------------------------------------===/
00572 
00573 void RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
00574                                    const char* nl, const char *sep) {
00575 
00576   ConstraintRangeTy Ranges = St->get<ConstraintRange>();
00577 
00578   if (Ranges.isEmpty()) {
00579     Out << nl << sep << "Ranges are empty." << nl;
00580     return;
00581   }
00582 
00583   Out << nl << sep << "Ranges of symbol values:";
00584   for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
00585     Out << nl << ' ' << I.getKey() << " : ";
00586     I.getData().print(Out);
00587   }
00588   Out << nl;
00589 }