about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-07-25 22:22:55 +0100
committerMartinNowack <martin.nowack@gmail.com>2019-07-30 21:40:30 +0100
commit9b3c98850572f0729afe97ffde16d05a7e6e691b (patch)
tree886a893600961d6d1287ea716f5c776597a65fc9 /lib/Core
parentd1f714b72da1674f6f784a8a1b2a6179f103b723 (diff)
downloadklee-9b3c98850572f0729afe97ffde16d05a7e6e691b.tar.gz
Consolidated Expr-related include files into a single include/klee/Expr directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/AddressSpace.cpp2
-rw-r--r--lib/Core/AddressSpace.h2
-rw-r--r--lib/Core/Context.cpp2
-rw-r--r--lib/Core/Context.h2
-rw-r--r--lib/Core/ExecutionState.cpp2
-rw-r--r--lib/Core/Executor.cpp10
-rw-r--r--lib/Core/Executor.h7
-rw-r--r--lib/Core/ExecutorUtil.cpp8
-rw-r--r--lib/Core/ImpliedValue.cpp11
-rw-r--r--lib/Core/ImpliedValue.h2
-rw-r--r--lib/Core/Memory.cpp5
-rw-r--r--lib/Core/Memory.h5
-rw-r--r--lib/Core/MemoryManager.cpp5
-rw-r--r--lib/Core/PTree.cpp6
-rw-r--r--lib/Core/PTree.h2
-rw-r--r--lib/Core/SeedInfo.cpp4
-rw-r--r--lib/Core/SeedInfo.h2
-rw-r--r--lib/Core/TimingSolver.h2
18 files changed, 39 insertions, 40 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index fdf9c905..1a88e4ec 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -12,7 +12,7 @@
 #include "Memory.h"
 #include "TimingSolver.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/TimerStatIncrementer.h"
 
 using namespace klee;
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index d8ba6f36..9e7e414a 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -12,7 +12,7 @@
 
 #include "ObjectHolder.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/ADT/ImmutableMap.h"
 #include "klee/Internal/System/Time.h"
 
diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp
index 8246e631..a74d5446 100644
--- a/lib/Core/Context.cpp
+++ b/lib/Core/Context.cpp
@@ -9,7 +9,7 @@
 
 #include "Context.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include "llvm/IR/Type.h"
 #include "llvm/IR/DerivedTypes.h"
diff --git a/lib/Core/Context.h b/lib/Core/Context.h
index b2ea83f1..ecef646e 100644
--- a/lib/Core/Context.h
+++ b/lib/Core/Context.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_CONTEXT_H
 #define KLEE_CONTEXT_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 namespace klee {
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 3bce274c..15003b0e 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -11,7 +11,7 @@
 
 #include "klee/ExecutionState.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/InstructionInfoTable.h"
 #include "klee/Internal/Module/KInstruction.h"
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 330665c0..5590af41 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -28,7 +28,11 @@
 #include "klee/Common.h"
 #include "klee/Config/Version.h"
 #include "klee/ExecutionState.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprPPrinter.h"
+#include "klee/Expr/ExprSMTLIBPrinter.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/ADT/RNG.h"
 #include "klee/Internal/Module/Cell.h"
@@ -46,10 +50,6 @@
 #include "klee/SolverCmdLine.h"
 #include "klee/SolverStats.h"
 #include "klee/TimerStatIncrementer.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/ExprPPrinter.h"
-#include "klee/util/ExprSMTLIBPrinter.h"
-#include "klee/util/ExprUtil.h"
 #include "klee/util/GetElementPtrTypeIterator.h"
 
 #include "llvm/ADT/SmallPtrSet.h"
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index eafdc2f7..e2aab56c 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -16,17 +16,18 @@
 #define KLEE_EXECUTOR_H
 
 #include "klee/ExecutionState.h"
-#include "klee/Interpreter.h"
+#include "klee/Expr/ArrayCache.h"
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/System/Time.h"
-#include "klee/util/ArrayCache.h"
-#include "llvm/Support/raw_ostream.h"
+#include "klee/Interpreter.h"
 
 #include "llvm/ADT/Twine.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include "../Expr/ArrayExprOptimizer.h"
+
 #include <map>
 #include <memory>
 #include <set>
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 7b227eba..15125fe1 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -11,14 +11,12 @@
 
 #include "Context.h"
 
-#include "klee/Expr.h"
-#include "klee/Interpreter.h"
-#include "klee/Solver.h"
-
 #include "klee/Config/Version.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Module/KModule.h"
-
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/Interpreter.h"
+#include "klee/Solver.h"
 
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/DataLayout.h"
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 90000683..cc001660 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -10,13 +10,12 @@
 #include "ImpliedValue.h"
 
 #include "Context.h"
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
-#include "klee/Solver.h"
-// FIXME: Use APInt.
-#include "klee/Internal/Support/IntEvaluation.h"
 
-#include "klee/util/ExprUtil.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprUtil.h"
+#include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt
+#include "klee/Solver.h"
 
 #include <map>
 #include <set>
diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h
index 2b323c01..5943e41f 100644
--- a/lib/Core/ImpliedValue.h
+++ b/lib/Core/ImpliedValue.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_IMPLIEDVALUE_H
 #define KLEE_IMPLIEDVALUE_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include <vector>
 
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 9348105e..93be1f44 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -12,11 +12,12 @@
 #include "Context.h"
 #include "MemoryManager.h"
 #include "ObjectHolder.h"
-#include "klee/Expr.h"
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
 #include "klee/Solver.h"
-#include "klee/util/ArrayCache.h"
 #include "klee/util/BitArray.h"
 
 #include "llvm/IR/Function.h"
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 3558c96c..dfda433c 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -12,12 +12,13 @@
 
 #include "Context.h"
 #include "TimingSolver.h"
-#include "klee/Expr.h"
+
+#include "klee/Expr/Expr.h"
 
 #include "llvm/ADT/StringExtras.h"
 
-#include <vector>
 #include <string>
+#include <vector>
 
 namespace llvm {
   class Value;
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index dba90f8d..af3a2f26 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -7,11 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "MemoryManager.h"
+
 #include "CoreStats.h"
 #include "Memory.h"
-#include "MemoryManager.h"
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index e3e38868..732dc817 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -9,15 +9,13 @@
 
 #include "PTree.h"
 
-#include <klee/Expr.h>
-#include <klee/util/ExprPPrinter.h>
+#include <klee/Expr/Expr.h>
+#include <klee/Expr/ExprPPrinter.h>
 
 #include <vector>
 
 using namespace klee;
 
-  /* *** */
-
 PTree::PTree(const data_type &root) : root(new Node(nullptr, root)) {}
 
 std::pair<PTreeNode*, PTreeNode*>
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index b13b1d67..3185203f 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_PTREE_H
 #define KLEE_PTREE_H
 
-#include <klee/Expr.h>
+#include <klee/Expr/Expr.h>
 
 namespace klee {
   class ExecutionState;
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 90de17ff..a896197b 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -12,8 +12,8 @@
 #include "TimingSolver.h"
 
 #include "klee/ExecutionState.h"
-#include "klee/Expr.h"
-#include "klee/util/ExprUtil.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 
diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h
index 0d2b6ae0..fb2d025d 100644
--- a/lib/Core/SeedInfo.h
+++ b/lib/Core/SeedInfo.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_SEEDINFO_H
 #define KLEE_SEEDINFO_H
 
-#include "klee/util/Assignment.h"
+#include "klee/Expr/Assignment.h"
 
 extern "C" {
   struct KTest;
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 6951a3ad..b08073ab 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_TIMINGSOLVER_H
 #define KLEE_TIMINGSOLVER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Solver.h"
 #include "klee/Internal/System/Time.h"