aboutsummaryrefslogtreecommitdiffhomepage
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 {