diff options
79 files changed, 206 insertions, 201 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> 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" diff --git a/lib/Expr/ArrayCache.cpp b/lib/Expr/ArrayCache.cpp index b669f237..d4e8ee8f 100644 --- a/lib/Expr/ArrayCache.cpp +++ b/lib/Expr/ArrayCache.cpp @@ -1,4 +1,4 @@ -#include "klee/util/ArrayCache.h" +#include "klee/Expr/ArrayCache.h" namespace klee { diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 43b289e2..1a48adfe 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -13,10 +13,10 @@ #include "AssignmentGenerator.h" #include "klee/Config/Version.h" -#include "klee/ExprBuilder.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/ExprBuilder.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" -#include "klee/util/Assignment.h" #include "klee/util/BitArray.h" #include <llvm/ADT/APInt.h> diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h index 8f6472a4..ca90931d 100644 --- a/lib/Expr/ArrayExprOptimizer.h +++ b/lib/Expr/ArrayExprOptimizer.h @@ -17,7 +17,7 @@ #include <utility> #include <vector> -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/util/Ref.h" namespace klee { diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h index a0ee9f1d..098cb0a6 100644 --- a/lib/Expr/ArrayExprRewriter.h +++ b/lib/Expr/ArrayExprRewriter.h @@ -14,7 +14,7 @@ #include <map> #include <vector> -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/util/Ref.h" namespace klee { diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h index bfa75478..a6d9ae46 100644 --- a/lib/Expr/ArrayExprVisitor.h +++ b/lib/Expr/ArrayExprVisitor.h @@ -10,9 +10,9 @@ #ifndef KLEE_ARRAYEXPRVISITOR_H #define KLEE_ARRAYEXPRVISITOR_H -#include "klee/ExprBuilder.h" +#include "klee/Expr/ExprBuilder.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/SolverCmdLine.h" -#include "klee/util/ExprVisitor.h" #include <unordered_map> #include <unordered_set> diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp index d788785a..2fc569cc 100644 --- a/lib/Expr/Assigment.cpp +++ b/lib/Expr/Assigment.cpp @@ -6,7 +6,9 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/util/Assignment.h" + +#include "klee/Expr/Assignment.h" + namespace klee { void Assignment::dump() { diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp index dc744ba0..acb2dc13 100644 --- a/lib/Expr/AssignmentGenerator.cpp +++ b/lib/Expr/AssignmentGenerator.cpp @@ -9,21 +9,22 @@ #include "AssignmentGenerator.h" -#include <cassert> -#include <cstdint> +#include "klee/Expr/Assignment.h" +#include "klee/Internal/Support/ErrorHandling.h" +#include "klee/klee.h" + #include <llvm/ADT/APInt.h> #include <llvm/Support/Casting.h> #include <llvm/Support/raw_ostream.h> + +#include <cassert> +#include <cstdint> #include <map> #include <set> #include <stddef.h> #include <string> #include <utility> -#include "klee/Internal/Support/ErrorHandling.h" -#include "klee/klee.h" -#include "klee/util/Assignment.h" - using namespace klee; bool AssignmentGenerator::generatePartialAssignment(const ref<Expr> &e, diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h index 3bd940e7..173b863e 100644 --- a/lib/Expr/AssignmentGenerator.h +++ b/lib/Expr/AssignmentGenerator.h @@ -10,11 +10,11 @@ #ifndef KLEE_ASSIGNMENTGENERATOR_H #define KLEE_ASSIGNMENTGENERATOR_H -#include <vector> - -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/util/Ref.h" +#include <vector> + namespace klee { class Assignment; } /* namespace klee */ diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index e033333b..2b5adc4c 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -7,12 +7,12 @@ // //===----------------------------------------------------------------------===// -#include "klee/Constraints.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprPPrinter.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/Internal/Module/KModule.h" #include "klee/OptionCategories.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ExprVisitor.h" #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 060595d6..6b8dc95f 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -7,14 +7,14 @@ // //===----------------------------------------------------------------------===// -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Config/Version.h" +#include "klee/Expr/ExprPPrinter.h" // FIXME: We shouldn't need this once fast constant support moves into // Core. If we need to do arithmetic, we probably want to use APInt. #include "klee/Internal/Support/IntEvaluation.h" #include "klee/OptionCategories.h" -#include "klee/util/ExprPPrinter.h" #include "llvm/ADT/Hashing.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp index d9e20e45..e1cfa2d2 100644 --- a/lib/Expr/ExprBuilder.cpp +++ b/lib/Expr/ExprBuilder.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/ExprBuilder.h" +#include "klee/Expr/ExprBuilder.h" using namespace klee; diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp index 6b84cd6f..f03d7669 100644 --- a/lib/Expr/ExprEvaluator.cpp +++ b/lib/Expr/ExprEvaluator.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprEvaluator.h" +#include "klee/Expr/ExprEvaluator.h" using namespace klee; diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 114c46b4..2ccd7262 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -7,9 +7,9 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprPPrinter.h" +#include "klee/Expr/ExprPPrinter.h" -#include "klee/Constraints.h" +#include "klee/Expr/Constraints.h" #include "klee/OptionCategories.h" #include "klee/util/PrintContext.h" diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index 06186db2..b83a6af4 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprSMTLIBPrinter.h" +#include "klee/Expr/ExprSMTLIBPrinter.h" #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 2106b226..911366f3 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -7,12 +7,10 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprUtil.h" -#include "klee/util/ExprHashMap.h" - -#include "klee/Expr.h" - -#include "klee/util/ExprVisitor.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/ExprVisitor.h" #include <set> diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp index b99cc7e7..a3fa41d8 100644 --- a/lib/Expr/ExprVisitor.cpp +++ b/lib/Expr/ExprVisitor.cpp @@ -7,9 +7,10 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprVisitor.h" +#include "klee/Expr/ExprVisitor.h" + +#include "klee/Expr/Expr.h" -#include "klee/Expr.h" #include "llvm/Support/CommandLine.h" namespace { diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp index e250a968..784764bb 100644 --- a/lib/Expr/Lexer.cpp +++ b/lib/Expr/Lexer.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "expr/Lexer.h" +#include "klee/Expr/Parser/Lexer.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 479ff6c2..c365002d 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -7,16 +7,14 @@ // //===----------------------------------------------------------------------===// -#include "expr/Parser.h" - -#include "expr/Lexer.h" - #include "klee/Config/Version.h" -#include "klee/Constraints.h" -#include "klee/ExprBuilder.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/ExprBuilder.h" +#include "klee/Expr/ExprPPrinter.h" +#include "klee/Expr/Parser/Lexer.h" +#include "klee/Expr/Parser/Parser.h" #include "klee/Solver.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ArrayCache.h" #include "llvm/ADT/APInt.h" #include "llvm/Support/MemoryBuffer.h" diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index d58a3642..7264ca89 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -7,14 +7,12 @@ // //===----------------------------------------------------------------------===// -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include <cassert> using namespace klee; -/// - UpdateNode::UpdateNode(const UpdateNode *_next, const ref<Expr> &_index, const ref<Expr> &_value) diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index 82702dbf..b75f982a 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -6,10 +6,12 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/util/Assignment.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Assignment.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" + #include <vector> namespace klee { diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index a6ca93ac..2eedc616 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -10,8 +10,8 @@ #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" #include "klee/IncompleteSolver.h" #include "klee/SolverImpl.h" diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index d2e080d9..5c181dc3 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -9,17 +9,17 @@ #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/Internal/ADT/MapOfSets.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/SolverImpl.h" #include "klee/SolverStats.h" #include "klee/TimerStatIncrementer.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" -#include "klee/util/ExprVisitor.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 5ea6c1d4..9f493cd1 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -10,27 +10,25 @@ #define DEBUG_TYPE "cex-solver" #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprEvaluator.h" +#include "klee/Expr/ExprRangeEvaluator.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/IncompleteSolver.h" -#include "klee/util/ExprEvaluator.h" -#include "klee/util/ExprRangeEvaluator.h" -#include "klee/util/ExprVisitor.h" -// FIXME: Use APInt. #include "klee/Internal/Support/Debug.h" -#include "klee/Internal/Support/IntEvaluation.h" +#include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt #include "llvm/Support/raw_ostream.h" -#include <sstream> + #include <cassert> #include <map> +#include <sstream> #include <vector> using namespace klee; -/***/ - - // Hacker's Delight, pgs 58-63 +// Hacker's Delight, pgs 58-63 static uint64_t minOR(uint64_t a, uint64_t b, uint64_t c, uint64_t d) { uint64_t temp, m = ((uint64_t) 1)<<63; diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index 72fe2a95..e19a71e1 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -9,7 +9,7 @@ #include "klee/IncompleteSolver.h" -#include "klee/Constraints.h" +#include "klee/Expr/Constraints.h" using namespace klee; using namespace llvm; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 447e5575..12017e5c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -10,19 +10,19 @@ #define DEBUG_TYPE "independent-solver" #include "klee/Solver.h" -#include "klee/Expr.h" -#include "klee/Constraints.h" -#include "klee/SolverImpl.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/Debug.h" - -#include "klee/util/ExprUtil.h" -#include "klee/util/Assignment.h" +#include "klee/SolverImpl.h" #include "llvm/Support/raw_ostream.h" + +#include <list> #include <map> -#include <vector> #include <ostream> -#include <list> +#include <vector> using namespace klee; using namespace llvm; diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp index 0c2ac6dd..27e8ad0b 100644 --- a/lib/Solver/KQueryLoggingSolver.cpp +++ b/lib/Solver/KQueryLoggingSolver.cpp @@ -9,14 +9,12 @@ #include "QueryLoggingSolver.h" -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprPPrinter.h" #include "klee/Internal/System/Time.h" using namespace klee; -/// - class KQueryLoggingSolver : public QueryLoggingSolver { private : diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index ffe4608d..3112495d 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -7,23 +7,17 @@ // //===----------------------------------------------------------------------===// -/* - * MetaSMTBuilder.h - * - * Created on: 8 Aug 2012 - * Author: hpalikar - */ - #ifndef KLEE_METASMTBUILDER_H #define KLEE_METASMTBUILDER_H -#include "klee/Config/config.h" -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ArrayExprHash.h" -#include "klee/util/ExprHashMap.h" #include "ConstantDivision.h" +#include "klee/Config/config.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/ExprPPrinter.h" + #ifdef ENABLE_METASMT #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index dfa78e42..c4ff1f13 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -7,16 +7,17 @@ // //===----------------------------------------------------------------------===// #include "klee/Config/config.h" -#ifdef ENABLE_METASMT +#ifdef ENABLE_METASMT #include "MetaSMTSolver.h" #include "MetaSMTBuilder.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/ErrorHandling.h" @@ -51,11 +52,11 @@ #endif #include <errno.h> -#include <unistd.h> #include <signal.h> -#include <sys/wait.h> #include <sys/ipc.h> #include <sys/shm.h> +#include <sys/wait.h> +#include <unistd.h> static unsigned char *shared_memory_ptr; static int shared_memory_id = 0; diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index f734ac38..bfea5c1b 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -8,7 +8,8 @@ //===----------------------------------------------------------------------===// #include "QueryLoggingSolver.h" -#include "klee/util/ExprSMTLIBPrinter.h" + +#include "klee/Expr/ExprSMTLIBPrinter.h" using namespace klee; diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 0bd5084a..645c8989 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -10,10 +10,10 @@ #ifdef ENABLE_STP #include "STPBuilder.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Solver.h" -#include "klee/util/Bits.h" #include "klee/SolverStats.h" +#include "klee/util/Bits.h" #include "ConstantDivision.h" diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index cb163384..814046fa 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -10,9 +10,9 @@ #ifndef KLEE_STPBUILDER_H #define KLEE_STPBUILDER_H -#include "klee/util/ExprHashMap.h" -#include "klee/util/ArrayExprHash.h" #include "klee/Config/config.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" #include <vector> diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index e8b9222f..eb46b6db 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -9,23 +9,25 @@ #include "klee/Config/config.h" #ifdef ENABLE_STP + #include "STPBuilder.h" #include "STPSolver.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/SolverImpl.h" -#include "klee/Internal/Support/ErrorHandling.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" #include <csignal> -#include <unistd.h> #include <sys/ipc.h> #include <sys/shm.h> #include <sys/wait.h> +#include <unistd.h> namespace { diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 4f7458c5..6c7361dc 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -8,8 +8,9 @@ //===----------------------------------------------------------------------===// #include "klee/Solver.h" + +#include "klee/Expr/Constraints.h" #include "klee/SolverImpl.h" -#include "klee/Constraints.h" using namespace klee; diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 40a7c9e0..71e6834e 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -6,9 +6,11 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" + #include <vector> namespace klee { diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 06b995ae..07a7b681 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -10,7 +10,7 @@ #ifdef ENABLE_Z3 #include "Z3Builder.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverStats.h" diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index efbf4f9a..4501ecbd 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -11,8 +11,9 @@ #define KLEE_Z3BUILDER_H #include "klee/Config/config.h" -#include "klee/util/ArrayExprHash.h" -#include "klee/util/ExprHashMap.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" + #include <unordered_map> #include <z3.h> diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 74fee290..cfcb77e7 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -6,19 +6,22 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// + #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/Support/FileHandling.h" #include "klee/OptionCategories.h" #ifdef ENABLE_Z3 + #include "Z3Solver.h" #include "Z3Builder.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 9033a2b4..cc292d10 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -7,23 +7,22 @@ // //===----------------------------------------------------------------------===// -#include "expr/Lexer.h" -#include "expr/Parser.h" - #include "klee/Common.h" #include "klee/Config/Version.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" -#include "klee/ExprBuilder.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprBuilder.h" +#include "klee/Expr/ExprPPrinter.h" +#include "klee/Expr/ExprSMTLIBPrinter.h" +#include "klee/Expr/ExprVisitor.h" +#include "klee/Expr/Parser/Lexer.h" +#include "klee/Expr/Parser/Parser.h" #include "klee/Internal/Support/PrintVersion.h" #include "klee/OptionCategories.h" #include "klee/Solver.h" #include "klee/SolverCmdLine.h" #include "klee/SolverImpl.h" #include "klee/Statistics.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ExprSMTLIBPrinter.h" -#include "klee/util/ExprVisitor.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 99a9bf2a..8235c261 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -11,7 +11,7 @@ #include "klee/Config/Version.h" #include "klee/ExecutionState.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/TreeStream.h" #include "klee/Internal/Support/Debug.h" diff --git a/unittests/Assignment/AssignmentTest.cpp b/unittests/Assignment/AssignmentTest.cpp index 0eaa28f1..872d3301 100644 --- a/unittests/Assignment/AssignmentTest.cpp +++ b/unittests/Assignment/AssignmentTest.cpp @@ -1,6 +1,8 @@ -#include "klee/util/ArrayCache.h" -#include "klee/util/Assignment.h" #include "gtest/gtest.h" + +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/Assignment.h" + #include <iostream> #include <vector> diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp index fba15535..3a7541e9 100644 --- a/unittests/Expr/ExprTest.cpp +++ b/unittests/Expr/ExprTest.cpp @@ -10,8 +10,8 @@ #include <iostream> #include "gtest/gtest.h" -#include "klee/Expr.h" -#include "klee/util/ArrayCache.h" +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/Expr.h" using namespace klee; diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index b178ced3..b15fd64b 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -7,16 +7,18 @@ // //===----------------------------------------------------------------------===// -#include <iostream> #include "gtest/gtest.h" -#include "klee/SolverCmdLine.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" #include "klee/Solver.h" -#include "klee/util/ArrayCache.h" +#include "klee/SolverCmdLine.h" + #include "llvm/ADT/StringExtras.h" +#include <iostream> + using namespace klee; namespace { |