about summary refs log tree commit diff homepage
path: root/include
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 /include
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 'include')
-rw-r--r--include/klee/ExecutionState.h4
-rw-r--r--include/klee/Expr/ArrayCache.h (renamed from include/klee/util/ArrayCache.h)4
-rw-r--r--include/klee/Expr/ArrayExprHash.h (renamed from include/klee/util/ArrayExprHash.h)2
-rw-r--r--include/klee/Expr/Assignment.h (renamed from include/klee/util/Assignment.h)6
-rw-r--r--include/klee/Expr/Constraints.h (renamed from include/klee/Constraints.h)2
-rw-r--r--include/klee/Expr/Expr.h (renamed from include/klee/Expr.h)0
-rw-r--r--include/klee/Expr/ExprBuilder.h (renamed from include/klee/ExprBuilder.h)0
-rw-r--r--include/klee/Expr/ExprEvaluator.h (renamed from include/klee/util/ExprEvaluator.h)4
-rw-r--r--include/klee/Expr/ExprHashMap.h (renamed from include/klee/util/ExprHashMap.h)2
-rw-r--r--include/klee/Expr/ExprPPrinter.h (renamed from include/klee/util/ExprPPrinter.h)2
-rw-r--r--include/klee/Expr/ExprRangeEvaluator.h (renamed from include/klee/util/ExprRangeEvaluator.h)2
-rw-r--r--include/klee/Expr/ExprSMTLIBPrinter.h (renamed from include/klee/util/ExprSMTLIBPrinter.h)13
-rw-r--r--include/klee/Expr/ExprUtil.h (renamed from include/klee/util/ExprUtil.h)3
-rw-r--r--include/klee/Expr/ExprVisitor.h (renamed from include/klee/util/ExprVisitor.h)0
-rw-r--r--include/klee/Expr/Parser/Lexer.h (renamed from include/expr/Lexer.h)0
-rw-r--r--include/klee/Expr/Parser/Parser.h (renamed from include/expr/Parser.h)2
-rw-r--r--include/klee/Internal/Module/Cell.h2
-rw-r--r--include/klee/Solver.h2
-rw-r--r--include/klee/util/PrintContext.h4
19 files changed, 28 insertions, 26 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index e2c6bffe..891e6f06 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_EXECUTIONSTATE_H
 #define KLEE_EXECUTIONSTATE_H
 
-#include "klee/Constraints.h"
-#include "klee/Expr.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/Expr.h"
 #include "klee/Internal/ADT/TreeStream.h"
 #include "klee/Internal/System/Time.h"
 #include "klee/MergeHandler.h"
diff --git a/include/klee/util/ArrayCache.h b/include/klee/Expr/ArrayCache.h
index bec6e15a..09eddf49 100644
--- a/include/klee/util/ArrayCache.h
+++ b/include/klee/Expr/ArrayCache.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_ARRAYCACHE_H
 #define KLEE_ARRAYCACHE_H
 
-#include "klee/Expr.h"
-#include "klee/util/ArrayExprHash.h" // For klee::ArrayHashFn
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ArrayExprHash.h" // For klee::ArrayHashFn
 
 // FIXME: Remove this hack when we switch to C++11
 #ifdef _LIBCPP_VERSION
diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/Expr/ArrayExprHash.h
index 05cb8692..04660fe0 100644
--- a/include/klee/util/ArrayExprHash.h
+++ b/include/klee/Expr/ArrayExprHash.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_ARRAYEXPRHASH_H
 #define KLEE_ARRAYEXPRHASH_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/TimerStatIncrementer.h"
 #include "klee/SolverStats.h"
 
diff --git a/include/klee/util/Assignment.h b/include/klee/Expr/Assignment.h
index 8d082791..ead459a9 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/Expr/Assignment.h
@@ -10,11 +10,9 @@
 #ifndef KLEE_ASSIGNMENT_H
 #define KLEE_ASSIGNMENT_H
 
-#include <map>
-
-#include "klee/util/ExprEvaluator.h"
+#include "klee/Expr/ExprEvaluator.h"
 
-// FIXME: Rename?
+#include <map>
 
 namespace klee {
   class Array;
diff --git a/include/klee/Constraints.h b/include/klee/Expr/Constraints.h
index 08077293..b9bf3464 100644
--- a/include/klee/Constraints.h
+++ b/include/klee/Expr/Constraints.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_CONSTRAINTS_H
 #define KLEE_CONSTRAINTS_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 // FIXME: Currently we use ConstraintManager for two things: to pass
 // sets of constraints around, and to optimize constraints. We should
diff --git a/include/klee/Expr.h b/include/klee/Expr/Expr.h
index d4e4f7fa..d4e4f7fa 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr/Expr.h
diff --git a/include/klee/ExprBuilder.h b/include/klee/Expr/ExprBuilder.h
index 4a2c5cf4..4a2c5cf4 100644
--- a/include/klee/ExprBuilder.h
+++ b/include/klee/Expr/ExprBuilder.h
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/Expr/ExprEvaluator.h
index ed366f77..e0368203 100644
--- a/include/klee/util/ExprEvaluator.h
+++ b/include/klee/Expr/ExprEvaluator.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_EXPREVALUATOR_H
 #define KLEE_EXPREVALUATOR_H
 
-#include "klee/Expr.h"
-#include "klee/util/ExprVisitor.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/ExprVisitor.h"
 
 namespace klee {
   class ExprEvaluator : public ExprVisitor {
diff --git a/include/klee/util/ExprHashMap.h b/include/klee/Expr/ExprHashMap.h
index 6477b7c9..2b0b3bda 100644
--- a/include/klee/util/ExprHashMap.h
+++ b/include/klee/Expr/ExprHashMap.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_EXPRHASHMAP_H
 #define KLEE_EXPRHASHMAP_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include <ciso646>
 #ifdef _LIBCPP_VERSION
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/Expr/ExprPPrinter.h
index f2537750..7541c132 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/Expr/ExprPPrinter.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_EXPRPPRINTER_H
 #define KLEE_EXPRPPRINTER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 namespace llvm {
   class raw_ostream;
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/Expr/ExprRangeEvaluator.h
index b3011827..4d212764 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/Expr/ExprRangeEvaluator.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_EXPRRANGEEVALUATOR_H
 #define KLEE_EXPRRANGEEVALUATOR_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/util/Bits.h"
 
 namespace klee {
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/Expr/ExprSMTLIBPrinter.h
index cf5df1c5..b042bfeb 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/Expr/ExprSMTLIBPrinter.h
@@ -11,13 +11,14 @@
 #ifndef KLEE_EXPRSMTLIBPRINTER_H
 #define KLEE_EXPRSMTLIBPRINTER_H
 
-#include <string>
-#include <set>
-#include <map>
-#include <klee/Constraints.h>
-#include <klee/Expr.h>
-#include <klee/util/PrintContext.h>
+#include <klee/Expr/Constraints.h>
+#include <klee/Expr/Expr.h>
 #include <klee/Solver.h>
+#include <klee/util/PrintContext.h>
+
+#include <map>
+#include <set>
+#include <string>
 
 namespace llvm {
 class raw_ostream;
diff --git a/include/klee/util/ExprUtil.h b/include/klee/Expr/ExprUtil.h
index 88db15f0..c6b2c2d7 100644
--- a/include/klee/util/ExprUtil.h
+++ b/include/klee/Expr/ExprUtil.h
@@ -10,7 +10,8 @@
 #ifndef KLEE_EXPRUTIL_H
 #define KLEE_EXPRUTIL_H
 
-#include "klee/util/ExprVisitor.h"
+#include "klee/Expr/ExprVisitor.h"
+
 #include <vector>
 
 namespace klee {
diff --git a/include/klee/util/ExprVisitor.h b/include/klee/Expr/ExprVisitor.h
index 03d4d77d..03d4d77d 100644
--- a/include/klee/util/ExprVisitor.h
+++ b/include/klee/Expr/ExprVisitor.h
diff --git a/include/expr/Lexer.h b/include/klee/Expr/Parser/Lexer.h
index 14ae7f85..14ae7f85 100644
--- a/include/expr/Lexer.h
+++ b/include/klee/Expr/Parser/Lexer.h
diff --git a/include/expr/Parser.h b/include/klee/Expr/Parser/Parser.h
index 6a34b8d0..c1888e26 100644
--- a/include/expr/Parser.h
+++ b/include/klee/Expr/Parser/Parser.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_PARSER_H
 #define KLEE_PARSER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 
 #include <vector>
 #include <string>
diff --git a/include/klee/Internal/Module/Cell.h b/include/klee/Internal/Module/Cell.h
index 691c1c89..abdce3f6 100644
--- a/include/klee/Internal/Module/Cell.h
+++ b/include/klee/Internal/Module/Cell.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_CELL_H
 #define KLEE_CELL_H
 
-#include <klee/Expr.h>
+#include <klee/Expr/Expr.h>
 
 namespace klee {
   class MemoryObject;
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 476fb732..f320a5b6 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_SOLVER_H
 #define KLEE_SOLVER_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
 #include "klee/SolverCmdLine.h"
 #include "klee/Internal/System/Time.h"
 
diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
index 9deaa207..de9094da 100644
--- a/include/klee/util/PrintContext.h
+++ b/include/klee/util/PrintContext.h
@@ -10,8 +10,10 @@
 #ifndef KLEE_PRINTCONTEXT_H
 #define KLEE_PRINTCONTEXT_H
 
-#include "klee/Expr.h"
+#include "klee/Expr/Expr.h"
+
 #include "llvm/Support/raw_ostream.h"
+
 #include <sstream>
 #include <string>
 #include <stack>