diff options
-rw-r--r-- | include/klee/SolverStats.h (renamed from lib/Solver/SolverStats.h) | 0 | ||||
-rw-r--r-- | include/klee/util/ArrayCache.h | 12 | ||||
-rw-r--r-- | include/klee/util/ArrayExprHash.h | 2 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 2 | ||||
-rw-r--r-- | lib/Core/StatsTracker.cpp | 2 | ||||
-rw-r--r-- | lib/Expr/Parser.cpp | 32 | ||||
-rw-r--r-- | lib/Solver/CachingSolver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/STPBuilder.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/SolverStats.cpp | 2 |
11 files changed, 42 insertions, 18 deletions
diff --git a/lib/Solver/SolverStats.h b/include/klee/SolverStats.h index a38c9826..a38c9826 100644 --- a/lib/Solver/SolverStats.h +++ b/include/klee/SolverStats.h diff --git a/include/klee/util/ArrayCache.h b/include/klee/util/ArrayCache.h index 3dd88a11..56d69df6 100644 --- a/include/klee/util/ArrayCache.h +++ b/include/klee/util/ArrayCache.h @@ -11,6 +11,7 @@ #define KLEE_ARRAY_CACHE_H #include "klee/Expr.h" +#include "klee/util/ArrayExprHash.h" // For klee::ArrayHashFn // FIXME: Remove this hack when we switch to C++11 #ifdef _LIBCPP_VERSION @@ -26,15 +27,6 @@ namespace klee { -// FIXME: This is copied from ``klee/util/ArrayExprHash.h``. -// We can't include it here becaues the includes are messed up -// in that file. -struct EquivArrayHashFn { - unsigned operator()(const Array *array) const { - return (array ? array->hash() : 0); - } -}; - struct EquivArrayCmpFn { bool operator()(const Array *array1, const Array *array2) const { if (array1 == NULL || array2 == NULL) @@ -76,7 +68,7 @@ public: Expr::Width _range = Expr::Int8); private: - typedef unordered_set<const Array *, klee::EquivArrayHashFn, + typedef unordered_set<const Array *, klee::ArrayHashFn, klee::EquivArrayCmpFn> ArrayHashMap; ArrayHashMap cachedSymbolicArrays; typedef std::vector<const Array *> ArrayPtrVec; diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h index da3b1d2b..23211a70 100644 --- a/include/klee/util/ArrayExprHash.h +++ b/include/klee/util/ArrayExprHash.h @@ -12,7 +12,7 @@ #include "klee/Expr.h" #include "klee/TimerStatIncrementer.h" -#include "SolverStats.h" +#include "klee/SolverStats.h" #include <map> diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 4a21be3e..9211f485 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -23,7 +23,6 @@ #include "UserSearcher.h" #include "ExecutorTimerInfo.h" -#include "../Solver/SolverStats.h" #include "klee/ExecutionState.h" #include "klee/Expr.h" @@ -47,6 +46,7 @@ #include "klee/Internal/Support/FloatEvaluation.h" #include "klee/Internal/System/Time.h" #include "klee/Internal/System/MemoryUsage.h" +#include "klee/SolverStats.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/IR/Function.h" diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 4633a5c5..2e107fb3 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -18,13 +18,13 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/SolverStats.h" #include "CallPathManager.h" #include "CoreStats.h" #include "Executor.h" #include "MemoryManager.h" #include "UserSearcher.h" -#include "../Solver/SolverStats.h" #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) #include "llvm/IR/BasicBlock.h" diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 854f6d52..e914cb80 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -331,6 +331,8 @@ namespace { MaxErrors(~0u), NumErrors(0) {} + virtual ~ParserImpl(); + /// Initialize - Initialize the parsing state. This must be called /// prior to the start of parsing. void Initialize() { @@ -1561,6 +1563,36 @@ void ParserImpl::Error(const char *Message, const Token &At) { llvm::errs() << '\n'; } +ParserImpl::~ParserImpl() { + // Free identifiers + // + // Note the Identifiers are not disjoint across the symbol + // tables so we need to keep track of what has freed to + // avoid doing a double free. + std::set<const Identifier*> freedNodes; + for (IdentifierTabTy::iterator pi = IdentifierTab.begin(), + pe = IdentifierTab.end(); + pi != pe; ++pi) { + const Identifier* id = pi->second; + if (freedNodes.insert(id).second) + delete id; + } + for (ExprSymTabTy::iterator pi = ExprSymTab.begin(), + pe = ExprSymTab.end(); + pi != pe; ++pi) { + const Identifier* id = pi->first; + if (freedNodes.insert(id).second) + delete id; + } + for (VersionSymTabTy::iterator pi = VersionSymTab.begin(), + pe = VersionSymTab.end(); + pi != pe; ++pi) { + const Identifier* id = pi->first; + if (freedNodes.insert(id).second) + delete id; + } +} + // AST API // FIXME: Move out of parser. diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index cfe08a96..1a6dce52 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -15,7 +15,7 @@ #include "klee/IncompleteSolver.h" #include "klee/SolverImpl.h" -#include "SolverStats.h" +#include "klee/SolverStats.h" #include <ciso646> #ifdef _LIBCPP_VERSION diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index fb07a6ec..8627b2ac 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -18,7 +18,7 @@ #include "klee/util/ExprVisitor.h" #include "klee/Internal/ADT/MapOfSets.h" -#include "SolverStats.h" +#include "klee/SolverStats.h" #include "klee/Internal/Support/ErrorHandling.h" diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 4bd0145f..2f51c2b9 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -12,9 +12,9 @@ #include "klee/Expr.h" #include "klee/Solver.h" #include "klee/util/Bits.h" +#include "klee/SolverStats.h" #include "ConstantDivision.h" -#include "SolverStats.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 341ca17c..6f4bbc5b 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -10,7 +10,6 @@ #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "SolverStats.h" #include "STPBuilder.h" #include "MetaSMTBuilder.h" @@ -23,6 +22,7 @@ #include "klee/Internal/Support/Timer.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/CommandLine.h" +#include "klee/SolverStats.h" #define vc_bvBoolExtract IAMTHESPAWNOFSATAN diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp index 9d6963cf..4b9c69c8 100644 --- a/lib/Solver/SolverStats.cpp +++ b/lib/Solver/SolverStats.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "SolverStats.h" +#include "klee/SolverStats.h" using namespace klee; |