about summary refs log tree commit diff homepage
path: root/lib/Expr/ArrayExprOptimizer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr/ArrayExprOptimizer.cpp')
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp18
1 files changed, 15 insertions, 3 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 0929efb5..dc0b2002 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -9,11 +9,23 @@
 
 #include "klee/ArrayExprOptimizer.h"
 
+#include <algorithm>
+#include <cassert>
+#include <llvm/ADT/APInt.h>
+#include <llvm/Support/Casting.h>
+#include <llvm/Support/CommandLine.h>
+#include <set>
+#include <stddef.h>
+
 #include "klee/ArrayExprRewriter.h"
+#include "klee/AssignmentGenerator.h"
+#include "klee/Config/Version.h"
+#include "klee/ExprBuilder.h"
+#include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/util/ArrayExprVisitor.h"
+#include "klee/util/Assignment.h"
 #include "klee/util/BitArray.h"
 
-#include <iostream>
-
 using namespace klee;
 
 namespace klee {
@@ -163,7 +175,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
     // For each concrete value 'i' stored in the array
     for (size_t aIdx = 0; aIdx < arr->constantValues.size(); aIdx += width) {
       Assignment *a = new Assignment();
-      v_arr_ty objects;
+      std::vector<const Array *> objects;
       std::vector<std::vector<unsigned char>> values;
 
       // For each symbolic index Expr(k) found