about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/SolverStats.h (renamed from lib/Solver/SolverStats.h)0
-rw-r--r--include/klee/util/ArrayCache.h12
-rw-r--r--include/klee/util/ArrayExprHash.h2
-rw-r--r--lib/Core/Executor.cpp2
-rw-r--r--lib/Core/StatsTracker.cpp2
-rw-r--r--lib/Expr/Parser.cpp32
-rw-r--r--lib/Solver/CachingSolver.cpp2
-rw-r--r--lib/Solver/CexCachingSolver.cpp2
-rw-r--r--lib/Solver/STPBuilder.cpp2
-rw-r--r--lib/Solver/Solver.cpp2
-rw-r--r--lib/Solver/SolverStats.cpp2
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;