diff options
author | Martin Nowack <martin.nowack@gmail.com> | 2018-05-15 15:10:16 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-07-04 15:13:02 +0100 |
commit | 6803c37be83f0c97c95870a18cb230e135a131c9 (patch) | |
tree | e42ae967f248014aa392ac1a985fc5a39203c789 /runtime/Intrinsic | |
parent | b25705f4d9cfdb4a7f9ecc4565cb31623f7bd38d (diff) | |
download | klee-6803c37be83f0c97c95870a18cb230e135a131c9.tar.gz |
Reorganise runtime libraries provided by KLEE
Strictly differentiate between the following type of libraries: * FreeStanding: contains minimal amount of methods a compiler would expect * klee-libc: contains a minimal libc implementation * POSIX: contains a POSIX layer that can be used on top of a libc implementation * Intrinsic: contains additional runtime functions which provide KLEE-specific functionalities, (e.g. checks) Builds always archives instead of single modules. This allows to reduce linked-in dependencies of tested applications.
Diffstat (limited to 'runtime/Intrinsic')
-rw-r--r-- | runtime/Intrinsic/Makefile.cmake.bitcode | 9 | ||||
-rw-r--r-- | runtime/Intrinsic/memcpy.c | 19 | ||||
-rw-r--r-- | runtime/Intrinsic/memmove.c | 28 | ||||
-rw-r--r-- | runtime/Intrinsic/mempcpy.c | 18 | ||||
-rw-r--r-- | runtime/Intrinsic/memset.c | 16 |
5 files changed, 1 insertions, 89 deletions
diff --git a/runtime/Intrinsic/Makefile.cmake.bitcode b/runtime/Intrinsic/Makefile.cmake.bitcode index 654ee020..77727fb4 100644 --- a/runtime/Intrinsic/Makefile.cmake.bitcode +++ b/runtime/Intrinsic/Makefile.cmake.bitcode @@ -10,13 +10,6 @@ LEVEL := ../ include $(LEVEL)/Makefile.cmake.bitcode.config -LLVMCC.Flags += -fno-builtin - -# FIXME: This is a horrible hack -ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1) - MODULE_NAME=kleeRuntimeIntrinsic -else - ARCHIVE_NAME=kleeRuntimeIntrinsic -endif +ARCHIVE_NAME=kleeRuntimeIntrinsic include $(LEVEL)/Makefile.cmake.bitcode.rules diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c deleted file mode 100644 index bd9f3e38..00000000 --- a/runtime/Intrinsic/memcpy.c +++ /dev/null @@ -1,19 +0,0 @@ -//===-- memcpy.c ----------------------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include <stdlib.h> - -__attribute__((weak)) void *memcpy(void *destaddr, void const *srcaddr, size_t len) { - char *dest = destaddr; - char const *src = srcaddr; - - while (len-- > 0) - *dest++ = *src++; - return destaddr; -} diff --git a/runtime/Intrinsic/memmove.c b/runtime/Intrinsic/memmove.c deleted file mode 100644 index e89abf7d..00000000 --- a/runtime/Intrinsic/memmove.c +++ /dev/null @@ -1,28 +0,0 @@ -//===-- memmove.c ---------------------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include <stdlib.h> - -__attribute__((weak)) void *memmove(void *dst, const void *src, size_t count) { - char *a = dst; - const char *b = src; - - if (src == dst) - return dst; - - if (src>dst) { - while (count--) *a++ = *b++; - } else { - a+=count-1; - b+=count-1; - while (count--) *a-- = *b--; - } - - return dst; -} diff --git a/runtime/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c deleted file mode 100644 index e47a94b1..00000000 --- a/runtime/Intrinsic/mempcpy.c +++ /dev/null @@ -1,18 +0,0 @@ -//===-- mempcpy.c ---------------------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include <stdlib.h> -__attribute__((weak)) void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { - char *dest = destaddr; - char const *src = srcaddr; - - while (len-- > 0) - *dest++ = *src++; - return dest; -} diff --git a/runtime/Intrinsic/memset.c b/runtime/Intrinsic/memset.c deleted file mode 100644 index c21f1fa9..00000000 --- a/runtime/Intrinsic/memset.c +++ /dev/null @@ -1,16 +0,0 @@ -//===-- memset.c ----------------------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include <stdlib.h> -__attribute__ ((weak)) void *memset(void * dst, int s, size_t count) { - volatile char * a = dst; - while (count-- > 0) - *a++ = s; - return dst; -} |