diff options
Diffstat (limited to 'lib/Core/MemoryManager.h')
-rw-r--r-- | lib/Core/MemoryManager.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h index d80e44af..5c5d21ca 100644 --- a/lib/Core/MemoryManager.h +++ b/lib/Core/MemoryManager.h @@ -27,8 +27,12 @@ namespace klee { objects_ty objects; ArrayCache *const arrayCache; + char *deterministicSpace; + char *nextFreeSlot; + size_t spaceSize; + public: - MemoryManager(ArrayCache *arrayCache) : arrayCache(arrayCache) {} + MemoryManager(ArrayCache *arrayCache); ~MemoryManager(); /** @@ -42,6 +46,11 @@ namespace klee { void deallocate(const MemoryObject *mo); void markFreed(MemoryObject *mo); ArrayCache *getArrayCache() const { return arrayCache; } + + /* + * Returns the size used by deterministic allocation in bytes + */ + size_t getUsedDeterministicSize(); }; } // End klee namespace |