aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
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 /lib
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.
Diffstat (limited to 'lib')
-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;
}