diff options
author | Dan Liew <delcypher@gmail.com> | 2014-04-24 14:14:22 +0100 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2014-04-24 14:14:22 +0100 |
commit | 9dd4766a3f58070501ed6498e6aa42c14776cc0f (patch) | |
tree | 01cfa9cf86783c002368e43197d92ca8b27f3925 /include | |
parent | 169b4eed5b29427611c7d4211de5c1ab16adb3cb (diff) | |
parent | 016120fd8a8a2cac8457b66b6d2a41e0b5093889 (diff) | |
download | klee-9dd4766a3f58070501ed6498e6aa42c14776cc0f.tar.gz |
Merge pull request #116 from MartinNowack/fix_malloc
Fix handling of memory usage in KLEE.
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Config/config.h.in | 3 | ||||
-rw-r--r-- | include/klee/Internal/System/MemoryUsage.h | 21 |
2 files changed, 24 insertions, 0 deletions
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index 3f6da802..5e49e35d 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -12,6 +12,9 @@ /* Define to 1 if you have the `stp' library (-lstp). */ #undef HAVE_LIBSTP +/* Define if mallinfo() is available on this platform. */ +#undef HAVE_MALLINFO + /* Define to 1 if you have the <memory.h> header file. */ #undef HAVE_MEMORY_H diff --git a/include/klee/Internal/System/MemoryUsage.h b/include/klee/Internal/System/MemoryUsage.h new file mode 100644 index 00000000..e8e5d769 --- /dev/null +++ b/include/klee/Internal/System/MemoryUsage.h @@ -0,0 +1,21 @@ +//===-- MemoryUsage.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_UTIL_MEMORYUSAGE_H +#define KLEE_UTIL_MEMORYUSAGE_H + +#include <cstddef> + +namespace klee { + namespace util { + size_t GetTotalMallocUsage(); + } +} + +#endif |