diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2012-01-18 18:58:10 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2012-01-18 18:58:10 +0000 |
commit | d32d0df34ab754d4d3b27b287092e536f03a231c (patch) | |
tree | 7d76e832672acd1ba11e2b3696b751d3baeee68a /include | |
parent | 5344817c3de946e0636f6f671749c464dc4c02f2 (diff) | |
download | klee-d32d0df34ab754d4d3b27b287092e536f03a231c.tar.gz |
Nice patch by Gang Hu, Heming Cui and Junfeng Yang fixing a memory
leak in KLEE. From Gang Hu: "The memory leak is caused by two reasons. First, the MemoryObject objects are not freed, until the MemoryManager is destroyed. Second, when KLEE allocates a non-fixed MemoryObject object, KLEE also allocates a block of memory which is the same as the object's size. This block of memory is never freed. So, this patch generally does reference counting on the MemoryObject objects, and frees them as soon as the reference count drops to zero." Many thanks to Paul Marinescu as well, who tested this patch thoroughly on the Coreutils benchmarks. On 1h runs, the memory consumption typically goes down by 1-5%, but some applications which see more significant gains. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@148402 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/ExecutionState.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 6523c456..720488cc 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -122,6 +122,8 @@ public: // use on structure ExecutionState(const std::vector<ref<Expr> > &assumptions); + ExecutionState(const ExecutionState& state); + ~ExecutionState(); ExecutionState *branch(); @@ -129,9 +131,7 @@ public: void pushFrame(KInstIterator caller, KFunction *kf); void popFrame(); - void addSymbolic(const MemoryObject *mo, const Array *array) { - symbolics.push_back(std::make_pair(mo, array)); - } + void addSymbolic(const MemoryObject *mo, const Array *array); void addConstraint(ref<Expr> e) { constraints.addConstraint(e); } |