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.h6
1 files changed, 5 insertions, 1 deletions
diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h
index 01683443..d80e44af 100644
--- a/lib/Core/MemoryManager.h
+++ b/lib/Core/MemoryManager.h
@@ -31,8 +31,12 @@ namespace klee {
     MemoryManager(ArrayCache *arrayCache) : arrayCache(arrayCache) {}
     ~MemoryManager();
 
+    /**
+     * Returns memory object which contains a handle to real virtual process
+     * memory.
+     */
     MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal,
-                           const llvm::Value *allocSite);
+                           const llvm::Value *allocSite, size_t alignment = 8);
     MemoryObject *allocateFixed(uint64_t address, uint64_t size,
                                 const llvm::Value *allocSite);
     void deallocate(const MemoryObject *mo);