about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2016-07-10 13:20:44 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2016-07-10 13:22:24 +0200
commitc7a2c02c6bdf038c94a28a0a3f787a1b09d83a62 (patch)
tree6c6a287ddcc01e3cbfd180238a5bc2bbc6452749
parent48797d9846c38406f31e8a933a28eeef480a664d (diff)
downloadklee-c7a2c02c6bdf038c94a28a0a3f787a1b09d83a62.tar.gz
Fix parsing of deterministic address.
Allows to provide 0 as an address to allocate deterministic memory
area at any free space.
-rw-r--r--lib/Core/MemoryManager.cpp7
1 files changed, 3 insertions, 4 deletions
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index 004ce090..f9f4b105 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -44,7 +44,7 @@ llvm::cl::opt<unsigned> RedZoneSpace(
                    "important to detect out-of-bound accesses (default=10)."),
     llvm::cl::init(10));
 
-llvm::cl::opt<uint64_t> DeterministicStartAddress(
+llvm::cl::opt<unsigned long long> DeterministicStartAddress(
     "allocate-determ-start-address",
     llvm::cl::desc("Start address for deterministic allocation. Has to be page "
                    "aligned (default=0x7ff30000000)."),
@@ -66,12 +66,11 @@ MemoryManager::MemoryManager(ArrayCache *_arrayCache)
     if (newSpace == MAP_FAILED) {
       klee_error("Couldn't mmap() memory for deterministic allocations");
     }
-    if (expectedAddress != newSpace) {
+    if (expectedAddress != newSpace && expectedAddress != 0) {
       klee_error("Could not allocate memory deterministically");
     }
 
-    klee_message("Deterministic memory allocation starting from %p",
-                 expectedAddress);
+    klee_message("Deterministic memory allocation starting from %p", newSpace);
     deterministicSpace = newSpace;
     nextFreeSlot = newSpace;
   }