about summary refs log tree commit diff homepage
path: root/lib/Core/MemoryManager.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/MemoryManager.h')
-rw-r--r--lib/Core/MemoryManager.h11
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