about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2018-10-18 12:41:07 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-10-23 18:53:46 +0300
commit6bd5d045f2cb19331feb34d7ea74f748c5568a91 (patch)
treeeb1147b7b7e5dc02d36011992f7311840fef95f6 /include
parenta72a2a9622aa05bd6eb1ffeb66e0db47b8cc4745 (diff)
downloadklee-6bd5d045f2cb19331feb34d7ea74f748c5568a91.tar.gz
Clean-up headers
Remove unneeded headers from include files
Diffstat (limited to 'include')
-rw-r--r--include/klee/ArrayExprOptimizer.h27
-rw-r--r--include/klee/ArrayExprRewriter.h25
-rw-r--r--include/klee/AssignmentGenerator.h12
3 files changed, 18 insertions, 46 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h
index 4836241d..aafe1d27 100644
--- a/include/klee/ArrayExprOptimizer.h
+++ b/include/klee/ArrayExprOptimizer.h
@@ -10,28 +10,15 @@
 #ifndef KLEE_EXPROPTIMIZER_H
 #define KLEE_EXPROPTIMIZER_H
 
-#include <cassert>
-#include <iterator>
+#include <cstdint>
 #include <map>
-#include <string>
+#include <unordered_map>
+#include <unordered_set>
 #include <utility>
 #include <vector>
 
 #include "Expr.h"
-#include "ExprBuilder.h"
-#include "Constraints.h"
-#include "Internal/Support/ErrorHandling.h"
-#include "util/ArrayExprVisitor.h"
-#include "util/Assignment.h"
 #include "util/Ref.h"
-#include "klee/AssignmentGenerator.h"
-#include "klee/ExecutionState.h"
-#include "klee/Config/Version.h"
-
-#include "llvm/Support/CommandLine.h"
-
-#include <unordered_map>
-#include <unordered_set>
 
 namespace klee {
 
@@ -42,10 +29,7 @@ enum ArrayOptimizationType {
   VALUE
 };
 
-class Expr;
-template <class T> class ref;
 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;
 
 class ExprOptimizer {
@@ -62,9 +46,8 @@ public:
   ref<Expr> optimizeExpr(const ref<Expr> &e, bool valueOnly);
 
 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,
+                      mapIndexOptimizedExpr_ty &idx_valIdx) const;
 
   ref<Expr> getSelectOptExpr(
       const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h
index 3828262a..2b6c78b4 100644
--- a/include/klee/ArrayExprRewriter.h
+++ b/include/klee/ArrayExprRewriter.h
@@ -10,31 +10,26 @@
 #ifndef LIB_EXPRREWRITER_H_
 #define LIB_EXPRREWRITER_H_
 
-#include "klee/Expr.h"
-#include "klee/CommandLine.h"
-#include "klee/Constraints.h"
-#include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/util/ArrayExprVisitor.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/Ref.h"
-#include "klee/AssignmentGenerator.h"
+#include <iterator>
+#include <map>
+#include <vector>
+
+#include "Expr.h"
+#include "util/Ref.h"
 
 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;
 
 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 mapIndexOptimizedExpr_ty &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);
+  static ref<Expr> rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
+                           const mapIndexOptimizedExpr_ty &idx_valIdx);
 
   static ref<Expr>
   concatenateOrExpr(const std::vector<ref<Expr>>::const_iterator begin,
diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h
index 96209498..404c8632 100644
--- a/include/klee/AssignmentGenerator.h
+++ b/include/klee/AssignmentGenerator.h
@@ -10,20 +10,14 @@
 #ifndef KLEE_ASSIGNMENTGENERATOR_H
 #define KLEE_ASSIGNMENTGENERATOR_H
 
-#include <cassert>
-#include <iterator>
-#include <map>
-#include <string>
-#include <utility>
 #include <vector>
 
 #include "Expr.h"
-#include "Constraints.h"
-#include "Internal/Support/ErrorHandling.h"
-#include "util/ArrayExprVisitor.h"
-#include "util/Assignment.h"
 #include "util/Ref.h"
 
+namespace klee {
+class Assignment;
+} /* namespace klee */
 
 namespace klee {