diff options
| author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-22 17:50:28 +0100 |
|---|---|---|
| committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-08 22:54:54 +0200 |
| commit | d06a14dc2ff22da34dbf566a2ad4626c88b0be17 (patch) | |
| tree | 1b31b82655a0c0003afa2a254aaba551cb67298e /lib/Solver/MetaSMTBuilder.h | |
| parent | ea0c6724dc992a5358d6da3d50d9f60472d66d64 (diff) | |
| download | klee-d06a14dc2ff22da34dbf566a2ad4626c88b0be17.tar.gz | |
Add deterministic allocation of memory
Deterministic allocation provides an internal allocator which
mmaps memory to a fixed static address.
This way, same allocation is assured across different KLEE runs
for the same application assuming a deterministic searcher.
In addition, this patch provides following options:
-allocate-determ: switch on/off deterministic allocation
-allocate-determ-size: adjust preallocated memory
-null-on-zero-malloc: returns null pointer in case a malloc
of size 0 was requested. According to standard, also a non-null pointer
can be returned (which happens with the default glibc malloc implementation)
-allocation-space: space between allocations can be adjusted. KLEE is not able
to detect out-of-bound accesses which are inside another but wrong object.
Due the implementation of typical allocators adjacent mallocs have space
in between for management purposes. This spaces helped KLEE to detect off-by-1/2 accesses.
For higher numbers, the allocation space has to be increased.
-allocate-determ-start-address: adjust deterministic start address. The addres
has to be page aligned. KLEE fails if it cannot acquire this address
Diffstat (limited to 'lib/Solver/MetaSMTBuilder.h')
0 files changed, 0 insertions, 0 deletions
