diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-10 13:20:44 +0200 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-10 13:22:24 +0200 |
commit | c7a2c02c6bdf038c94a28a0a3f787a1b09d83a62 (patch) | |
tree | 6c6a287ddcc01e3cbfd180238a5bc2bbc6452749 /lib/Core | |
parent | 48797d9846c38406f31e8a933a28eeef480a664d (diff) | |
download | klee-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/Core')
-rw-r--r-- | lib/Core/MemoryManager.cpp | 7 |
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; } |