Moved RangedConstraintManager header to the StaticAnalyser include dir

[mikhail.ramalho]

Summary

Moved RangedConstraintManager header from lib/StaticAnalyzer/Core/ to clang/StaticAnalyzer/Core/PathSensitive/. No changes to the code.

[mikhail.ramalho]

In the previous implementation, the Z3 wrapper classes were not inside the clang::ento namespace, and this patch doesn't change that.

Should it be part of the clang::ento namespace?

[mikhail.ramalho]

Moved CreateZ3ConstraintManager declaration to the Z3ConstraintManager.cpp.

[george.karpenkov]

Should it be part of the clang::ento namespace?

I would say yes.

[george.karpenkov]

Let's change the return type and add namespace (in my understanding it was previously not required as the class was not exposed).
Otherwise, looks good to me.

@ddcc any objections?

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1408 ↗

(On Diff #149502)

should we return a unique_ptr over Z3ConstraintManager now?

[mikhail.ramalho]

• Added Z3 wrapper classes to the clang::ento namespace

• Remove unnecessary headers from Z3ConstraintManager.h/.cpp

[george.karpenkov]

almost there, should we change the return type of CreateZ3ConstraintManager?

include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h

15 ↗

(On Diff #149510)

@ddcc BTW why are we using this header? It's comments explicitly state it should not be used by the application.

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1406 ↗

(On Diff #149510)

this is still returning a constraint manager

[mikhail.ramalho]

include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h

15 ↗

(On Diff #149510)

This is generated by cmake and we need it because it defines CLANG_ANALYZER_WITH_Z3, when CLANG_ANALYZER_BUILD_Z3=ON

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1408 ↗

(On Diff #149502)

CreateZ3ConstraintManager follows the same pattern of CreateRangeConstraintManager, defined in ConstraintManager.h.

They both return an unique_ptr<ConstraintManager> because neither Z3ConstraintManager nor RangeConstraintManager are defined in that header and the macro ANALYSIS_CONSTRAINTS in StaticAnalyzer/Core/Analyses.def expects a std::unique_ptr<clang::ento::ConstraintManager> (*)(clang::ento::ProgramStateManager&, clang::ento::SubEngine*).

[mikhail.ramalho]

It was not a problem before because the implementation was only in the cpp file. Any idea how we can make use of it now?

[george.karpenkov]

They both return an unique_ptr<ConstraintManager> because neither Z3ConstraintManager nor RangeConstraintManager are defined in that header

I think we could do something here either with forward declaration or with other tricks.
In any case, let's just commit this as is, and later I'll see whether we could get rid of the cast.

include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h

15 ↗

(On Diff #149510)

@mikhail.ramalho right, thanks, that sounds correct!

[mikhail.ramalho]

The config.h in the Z3ConstraintManager.h is a problem, we can't merge it like that.

The problem is when you do make install, the config.h header is not installed (because it's only relevant during compilation). So anyone using Z3ConstraintManager.h will get a compilation error due to the missing config.h header.

[george.karpenkov]

@mikhail.ramalho OK could we instead make sure that cmake would propagate the macro to the required translation unit?..
E.g. by adding -DCLANG_ANALYZER_WITH_Z3 to CFLAGS.

[george.karpenkov]

@mikhail.ramalho after giving it some more thought...

I think we should remove "#include<z3.h>" from Z3ConstraintManager.h. That might require fiddling with private functions, the easiest way would be to turn them into C static functions and move to the .cpp file. Then only the implementation file would require Z3 internals, and the header could be always included.

[george.karpenkov]

@mikhail.ramalho It might be even better to create a generic SMT-solver header (a subset of current Z3ConstraintManager.h).

Then we could use that instead, and move Z3ConstraintManager back to the implementation file.

It's actually a feature that the included header should not expose Z3 internals.

[mikhail.ramalho]

I agree, creating a generic SMT-solver header seems the best way forward in
the long run.

I'll start to work on it now.

[george.karpenkov]

I agree, creating a generic SMT-solver header seems the best way forward in the long run.

Right, but let's remember that we are under rather severe time pressure.
I strongly suggest to just take only the bare minimum of methods you need now (we just need to get a model and add range constraints, right?)

Others could be added later.

[ddcc]

In D47640#1119273, @george.karpenkov wrote:

@ddcc any objections?

The refactoring is fine with me.

In D47640#1119400, @george.karpenkov wrote:

It's actually a feature that the included header should not expose Z3 internals.

I agree that exposing the Z3* internal wrapper classes seems a bit excessive.

In D47640#1119432, @george.karpenkov wrote:

I agree, creating a generic SMT-solver header seems the best way forward in the long run.

Right, but let's remember that we are under rather severe time pressure.

If you plan to do a generic SMT-solver header, I'd suggest also pulling out the type inference and conversion code, since it should be in front of any SMT solver backend. But given the complexity, I'm fine with short-term fixes.

[mikhail.ramalho]

Split this patch in two, this one will only contain the RangedConstraintManager header change.

include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

+//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  Ranged constraint manager, built on SimpleConstraintManager.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
+
+namespace clang {
+
+namespace ento {
+
+/// A Range represents the closed range [from, to].  The caller must
+/// guarantee that from <= to.  Note that Range is immutable, so as not
+/// to subvert RangeSet's immutability.
+class Range : public std::pair<const llvm::APSInt *, const llvm::APSInt *> {
+public:
+  Range(const llvm::APSInt &from, const llvm::APSInt &to)
+      : std::pair<const llvm::APSInt *, const llvm::APSInt *>(&from, &to) {
+    assert(from <= to);
+  }
+  bool Includes(const llvm::APSInt &v) const {
+    return *first <= v && v <= *second;
+  }
+  const llvm::APSInt &From() const { return *first; }
+  const llvm::APSInt &To() const { return *second; }
+  const llvm::APSInt *getConcreteValue() const {
+    return &From() == &To() ? &From() : nullptr;
+  }
+
+  void Profile(llvm::FoldingSetNodeID &ID) const {
+    ID.AddPointer(&From());
+    ID.AddPointer(&To());
+  }
+};
+
+class RangeTrait : public llvm::ImutContainerInfo<Range> {
+public:
+  // When comparing if one Range is less than another, we should compare
+  // the actual APSInt values instead of their pointers.  This keeps the order
+  // consistent (instead of comparing by pointer values) and can potentially
+  // be used to speed up some of the operations in RangeSet.
+  static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
+    return *lhs.first < *rhs.first ||
+           (!(*rhs.first < *lhs.first) && *lhs.second < *rhs.second);
+  }
+};
+
+/// RangeSet contains a set of ranges. If the set is empty, then
+///  there the value of a symbol is overly constrained and there are no
+///  possible values for that symbol.
+class RangeSet {
+  typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
+  PrimRangeSet ranges; // no need to make const, since it is an
+                       // ImmutableSet - this allows default operator=
+                       // to work.
+public:
+  typedef PrimRangeSet::Factory Factory;
+  typedef PrimRangeSet::iterator iterator;
+
+  RangeSet(PrimRangeSet RS) : ranges(RS) {}
+
+  /// Create a new set with all ranges of this set and RS.
+  /// Possible intersections are not checked here.
+  RangeSet addRange(Factory &F, const RangeSet &RS) {
+    PrimRangeSet Ranges(RS.ranges);
+    for (const auto &range : ranges)
+      Ranges = F.add(Ranges, range);
+    return RangeSet(Ranges);
+  }
+
+  iterator begin() const { return ranges.begin(); }
+  iterator end() const { return ranges.end(); }
+
+  bool isEmpty() const { return ranges.isEmpty(); }
+
+  /// Construct a new RangeSet representing '{ [from, to] }'.
+  RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
+      : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
+
+  /// Profile - Generates a hash profile of this RangeSet for use
+  ///  by FoldingSet.
+  void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
+
+  /// getConcreteValue - If a symbol is contrained to equal a specific integer
+  ///  constant then this method returns that value.  Otherwise, it returns
+  ///  NULL.
+  const llvm::APSInt *getConcreteValue() const {
+    return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
+  }
+
+private:
+  void IntersectInRange(BasicValueFactory &BV, Factory &F,
+                        const llvm::APSInt &Lower, const llvm::APSInt &Upper,
+                        PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
+                        PrimRangeSet::iterator &e) const;
+
+  const llvm::APSInt &getMinValue() const;
+
+  bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const;
+
+public:
+  RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
+                     llvm::APSInt Upper) const;
+
+  void print(raw_ostream &os) const;
+
+  bool operator==(const RangeSet &other) const {
+    return ranges == other.ranges;
+  }
+};
+
+
+class ConstraintRange {};
+using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
+
+template <>
+struct ProgramStateTrait<ConstraintRange>
+  : public ProgramStatePartialTrait<ConstraintRangeTy> {
+  static void *GDMIndex() { static int Index; return &Index; }
+};
+
+
+class RangedConstraintManager : public SimpleConstraintManager {
+public:
+  RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
+
+  ~RangedConstraintManager() override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from SimpleConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                            bool Assumption) override;
+
+  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
+
+  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+                                       bool Assumption) override;
+
+protected:
+  /// Assume a constraint between a symbolic expression and a concrete integer.
+  virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
+                               BinaryOperator::Opcode op,
+                               const llvm::APSInt &Int);
+
+  //===------------------------------------------------------------------===//
+  // Interface that subclasses must implement.
+  //===------------------------------------------------------------------===//
+
+  // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
+  // operation for the method being invoked.
+
+  virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymWithinInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymOutsideInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+
+  //===------------------------------------------------------------------===//
+  // Internal implementation.
+  //===------------------------------------------------------------------===//
+private:
+  static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
+};
+
+} // end GR namespace
+
+} // end clang namespace
+
+#endif

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 //== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines RangeConstraintManager, a class that tracks simple
 //  equality and inequality constraints on symbolic values of ProgramState.
 //
 //===----------------------------------------------------------------------===//
 
-#include "RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
 #include "llvm/Support/raw_ostream.h"
 
 using namespace clang;
 using namespace ento;
 
 void RangeSet::IntersectInRange(BasicValueFactory &BV, Factory &F,

lib/StaticAnalyzer/Core/RangedConstraintManager.h

-//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
-//
-//                     The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-//  Ranged constraint manager, built on SimpleConstraintManager.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
-#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
-
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
-
-namespace clang {
-
-namespace ento {
-
-/// A Range represents the closed range [from, to].  The caller must
-/// guarantee that from <= to.  Note that Range is immutable, so as not
-/// to subvert RangeSet's immutability.
-class Range : public std::pair<const llvm::APSInt *, const llvm::APSInt *> {
-public:
-  Range(const llvm::APSInt &from, const llvm::APSInt &to)
-      : std::pair<const llvm::APSInt *, const llvm::APSInt *>(&from, &to) {
-    assert(from <= to);
-  }
-  bool Includes(const llvm::APSInt &v) const {
-    return *first <= v && v <= *second;
-  }
-  const llvm::APSInt &From() const { return *first; }
-  const llvm::APSInt &To() const { return *second; }
-  const llvm::APSInt *getConcreteValue() const {
-    return &From() == &To() ? &From() : nullptr;
-  }
-
-  void Profile(llvm::FoldingSetNodeID &ID) const {
-    ID.AddPointer(&From());
-    ID.AddPointer(&To());
-  }
-};
-
-class RangeTrait : public llvm::ImutContainerInfo<Range> {
-public:
-  // When comparing if one Range is less than another, we should compare
-  // the actual APSInt values instead of their pointers.  This keeps the order
-  // consistent (instead of comparing by pointer values) and can potentially
-  // be used to speed up some of the operations in RangeSet.
-  static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
-    return *lhs.first < *rhs.first ||
-           (!(*rhs.first < *lhs.first) && *lhs.second < *rhs.second);
-  }
-};
-
-/// RangeSet contains a set of ranges. If the set is empty, then
-///  there the value of a symbol is overly constrained and there are no
-///  possible values for that symbol.
-class RangeSet {
-  typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
-  PrimRangeSet ranges; // no need to make const, since it is an
-                       // ImmutableSet - this allows default operator=
-                       // to work.
-public:
-  typedef PrimRangeSet::Factory Factory;
-  typedef PrimRangeSet::iterator iterator;
-
-  RangeSet(PrimRangeSet RS) : ranges(RS) {}
-
-  /// Create a new set with all ranges of this set and RS.
-  /// Possible intersections are not checked here.
-  RangeSet addRange(Factory &F, const RangeSet &RS) {
-    PrimRangeSet Ranges(RS.ranges);
-    for (const auto &range : ranges)
-      Ranges = F.add(Ranges, range);
-    return RangeSet(Ranges);
-  }
-
-  iterator begin() const { return ranges.begin(); }
-  iterator end() const { return ranges.end(); }
-
-  bool isEmpty() const { return ranges.isEmpty(); }
-
-  /// Construct a new RangeSet representing '{ [from, to] }'.
-  RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
-      : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
-
-  /// Profile - Generates a hash profile of this RangeSet for use
-  ///  by FoldingSet.
-  void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
-
-  /// getConcreteValue - If a symbol is contrained to equal a specific integer
-  ///  constant then this method returns that value.  Otherwise, it returns
-  ///  NULL.
-  const llvm::APSInt *getConcreteValue() const {
-    return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
-  }
-
-private:
-  void IntersectInRange(BasicValueFactory &BV, Factory &F,
-                        const llvm::APSInt &Lower, const llvm::APSInt &Upper,
-                        PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
-                        PrimRangeSet::iterator &e) const;
-
-  const llvm::APSInt &getMinValue() const;
-
-  bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const;
-
-public:
-  RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
-                     llvm::APSInt Upper) const;
-
-  void print(raw_ostream &os) const;
-
-  bool operator==(const RangeSet &other) const {
-    return ranges == other.ranges;
-  }
-};
-
-
-class ConstraintRange {};
-using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
-
-template <>
-struct ProgramStateTrait<ConstraintRange>
-  : public ProgramStatePartialTrait<ConstraintRangeTy> {
-  static void *GDMIndex() { static int Index; return &Index; }
-};
-
-
-class RangedConstraintManager : public SimpleConstraintManager {
-public:
-  RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
-      : SimpleConstraintManager(SE, SB) {}
-
-  ~RangedConstraintManager() override;
-
-  //===------------------------------------------------------------------===//
-  // Implementation for interface from SimpleConstraintManager.
-  //===------------------------------------------------------------------===//
-
-  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
-                            bool Assumption) override;
-
-  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
-                                          const llvm::APSInt &From,
-                                          const llvm::APSInt &To,
-                                          bool InRange) override;
-
-  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
-                                       bool Assumption) override;
-
-protected:
-  /// Assume a constraint between a symbolic expression and a concrete integer.
-  virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
-                               BinaryOperator::Opcode op,
-                               const llvm::APSInt &Int);
-
-  //===------------------------------------------------------------------===//
-  // Interface that subclasses must implement.
-  //===------------------------------------------------------------------===//
-
-  // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
-  // operation for the method being invoked.
-
-  virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
-                                      const llvm::APSInt &V,
-                                      const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
-                                      const llvm::APSInt &V,
-                                      const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
-                                      const llvm::APSInt &V,
-                                      const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
-                                      const llvm::APSInt &V,
-                                      const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
-                                      const llvm::APSInt &V,
-                                      const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
-                                      const llvm::APSInt &V,
-                                      const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymWithinInclusiveRange(
-      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymOutsideInclusiveRange(
-      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
-
-  //===------------------------------------------------------------------===//
-  // Internal implementation.
-  //===------------------------------------------------------------------===//
-private:
-  static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
-};
-
-} // end GR namespace
-
-} // end clang namespace
-
-#endif

lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

 //== RangedConstraintManager.cpp --------------------------------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines RangedConstraintManager, a class that provides a
 //  range-based constraint manager interface.
 //
 //===----------------------------------------------------------------------===//
 
-#include "RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 
 namespace clang {
 
 namespace ento {
 
 RangedConstraintManager::~RangedConstraintManager() {}
 
 ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,