4 files changed, 62 insertions, 26 deletions

diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h
index 982136fb..9b62571f 100644
--- a/include/klee/ArrayExprOptimizer.h
+++ b/include/klee/ArrayExprOptimizer.h
@@ -1,3 +1,12 @@
+//===-- ArrayExprOptimizer.h ----------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #ifndef KLEE_EXPROPTIMIZER_H
 #define KLEE_EXPROPTIMIZER_H
 
@@ -52,39 +61,39 @@ extern llvm::cl::opt<double> ArrayValueSymbRatio;
 
 class Expr;
 template <class T> class ref;
-typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty;
+typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty;
 typedef std::vector<const Array *> v_arr_ty;
-typedef std::map<ref<Expr>, std::vector<ref<Expr> > > mapIndexOptimizedExpr_ty;
+typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty;
 
 class ExprOptimizer {
 private:
-  unordered_map<unsigned, ref<Expr> > cacheExprOptimized;
+  unordered_map<unsigned, ref<Expr>> cacheExprOptimized;
   unordered_set<unsigned> cacheExprUnapplicable;
-  unordered_map<unsigned, ref<Expr> > cacheReadExprOptimized;
+  unordered_map<unsigned, ref<Expr>> cacheReadExprOptimized;
 
 public:
   void optimizeExpr(const ref<Expr> &e, ref<Expr> &result,
                     bool valueOnly = false);
 
 private:
-  bool computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
-                      std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx)
-      const;
+  bool
+  computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
+                 std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx) const;
 
   ref<Expr> getSelectOptExpr(
       const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
-      std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo,
+      std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo,
       bool isSymbolic);
 
   ref<Expr> buildConstantSelectExpr(const ref<Expr> &index,
-                                   std::vector<uint64_t> &arrayValues,
-                                   Expr::Width width, unsigned elementsInArray) const;
+                                    std::vector<uint64_t> &arrayValues,
+                                    Expr::Width width,
+                                    unsigned elementsInArray) const;
 
   ref<Expr>
   buildMixedSelectExpr(const ReadExpr *re,
-                     std::vector<std::pair<uint64_t, bool> > &arrayValues,
-                     Expr::Width width, unsigned elementsInArray) const;
-
+                       std::vector<std::pair<uint64_t, bool>> &arrayValues,
+                       Expr::Width width, unsigned elementsInArray) const;
 };
 }
 
diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h
index dafcfef6..3828262a 100644
--- a/include/klee/ArrayExprRewriter.h
+++ b/include/klee/ArrayExprRewriter.h
@@ -1,3 +1,12 @@
+//===-- ArrayExprRewriter.h -----------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #ifndef LIB_EXPRREWRITER_H_
 #define LIB_EXPRREWRITER_H_
 
@@ -13,23 +22,23 @@
 namespace klee {
 
 typedef std::vector<const Array *> v_arr_ty;
-typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty;
-typedef std::map<ref<Expr>, std::vector<ref<Expr> > > mapIndexOptimizedExpr_ty;
+typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty;
+typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty;
 
 class ExprRewriter {
 public:
-  static ref<Expr> createOptExpr(
-      const ref<Expr> &e, const array2idx_ty &arrays,
-      const std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx);
+  static ref<Expr>
+  createOptExpr(const ref<Expr> &e, const array2idx_ty &arrays,
+                const std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx);
 
 private:
   static ref<Expr>
   rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
-          const std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx);
+          const std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx);
 
   static ref<Expr>
-  concatenateOrExpr(const std::vector<ref<Expr> >::const_iterator begin,
-                    const std::vector<ref<Expr> >::const_iterator end);
+  concatenateOrExpr(const std::vector<ref<Expr>>::const_iterator begin,
+                    const std::vector<ref<Expr>>::const_iterator end);
 
   static ref<Expr> createEqExpr(const ref<Expr> &index,
                                 const ref<Expr> &valIndex);
diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h
index 835651b8..aa228755 100644
--- a/include/klee/AssignmentGenerator.h
+++ b/include/klee/AssignmentGenerator.h
@@ -1,3 +1,12 @@
+//===-- AssignmentGenerator.h ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #ifndef KLEE_ASSIGNMENTGENERATOR_H
 #define KLEE_ASSIGNMENTGENERATOR_H
 
diff --git a/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h
index 70495989..6d7529e9 100644
--- a/include/klee/util/ArrayExprVisitor.h
+++ b/include/klee/util/ArrayExprVisitor.h
@@ -1,3 +1,12 @@
+//===-- ArrayExprVisitor.h ------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 #ifndef KLEE_ARRAYEXPRVISITOR_H_
 #define KLEE_ARRAYEXPRVISITOR_H_
 
@@ -33,7 +42,7 @@ public:
 //--------------------------- INDEX-BASED OPTIMIZATION-----------------------//
 class ConstantArrayExprVisitor : public ExprVisitor {
 private:
-  typedef std::map<const Array *, std::vector<ref<Expr> > > bindings_ty;
+  typedef std::map<const Array *, std::vector<ref<Expr>>> bindings_ty;
   bindings_ty &arrays;
   // Avoids adding the same index twice
   unordered_set<unsigned> addedIndexes;
@@ -91,7 +100,7 @@ public:
 class ArrayReadExprVisitor : public ExprVisitor {
 private:
   std::vector<const ReadExpr *> &reads;
-  std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo;
+  std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo;
   bool symbolic;
   bool incompatible;
 
@@ -104,7 +113,7 @@ protected:
 public:
   ArrayReadExprVisitor(
       std::vector<const ReadExpr *> &_reads,
-      std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &_readInfo)
+      std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &_readInfo)
       : ExprVisitor(true), reads(_reads), readInfo(_readInfo), symbolic(false),
         incompatible(false) {}
   inline bool isIncompatible() { return incompatible; }
@@ -114,14 +123,14 @@ public:
 class ArrayValueOptReplaceVisitor : public ExprVisitor {
 private:
   unordered_set<unsigned> visited;
-  std::map<unsigned, ref<Expr> > optimized;
+  std::map<unsigned, ref<Expr>> optimized;
 
 protected:
   Action visitConcat(const ConcatExpr &);
   Action visitRead(const ReadExpr &re);
 
 public:
-  ArrayValueOptReplaceVisitor(std::map<unsigned, ref<Expr> > &_optimized,
+  ArrayValueOptReplaceVisitor(std::map<unsigned, ref<Expr>> &_optimized,
                               bool recursive = true)
       : ExprVisitor(recursive), optimized(_optimized) {}
 };