diff options
Diffstat (limited to 'runtime')
-rw-r--r-- | runtime/Intrinsic/Makefile | 1 | ||||
-rw-r--r-- | runtime/Intrinsic/memcpy.c | 2 | ||||
-rw-r--r-- | runtime/Intrinsic/memmove.c | 2 | ||||
-rw-r--r-- | runtime/Intrinsic/mempcpy.c | 3 | ||||
-rw-r--r-- | runtime/Intrinsic/memset.c | 3 | ||||
-rwxr-xr-x | runtime/klee-libc/Makefile | 6 |
6 files changed, 9 insertions, 8 deletions
diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile index 849bfeee..3c6b01b3 100644 --- a/runtime/Intrinsic/Makefile +++ b/runtime/Intrinsic/Makefile @@ -17,6 +17,7 @@ BYTECODE_LIBRARY=1 DEBUG_RUNTIME=1 NO_PEDANTIC=1 +MODULE_NAME=kleeRuntimeIntrinsic C.Flags += -fno-builtin include $(LEVEL)/Makefile.common diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c index 7f7f133d..bd9f3e38 100644 --- a/runtime/Intrinsic/memcpy.c +++ b/runtime/Intrinsic/memcpy.c @@ -9,7 +9,7 @@ #include <stdlib.h> -void *memcpy(void *destaddr, void const *srcaddr, size_t len) { +__attribute__((weak)) void *memcpy(void *destaddr, void const *srcaddr, size_t len) { char *dest = destaddr; char const *src = srcaddr; diff --git a/runtime/Intrinsic/memmove.c b/runtime/Intrinsic/memmove.c index c6e1ada9..e89abf7d 100644 --- a/runtime/Intrinsic/memmove.c +++ b/runtime/Intrinsic/memmove.c @@ -9,7 +9,7 @@ #include <stdlib.h> -void *memmove(void *dst, const void *src, size_t count) { +__attribute__((weak)) void *memmove(void *dst, const void *src, size_t count) { char *a = dst; const char *b = src; diff --git a/runtime/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c index 31e142d9..e47a94b1 100644 --- a/runtime/Intrinsic/mempcpy.c +++ b/runtime/Intrinsic/mempcpy.c @@ -8,8 +8,7 @@ //===----------------------------------------------------------------------===// #include <stdlib.h> - -void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { +__attribute__((weak)) void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { char *dest = destaddr; char const *src = srcaddr; diff --git a/runtime/Intrinsic/memset.c b/runtime/Intrinsic/memset.c index bef85e6a..c21f1fa9 100644 --- a/runtime/Intrinsic/memset.c +++ b/runtime/Intrinsic/memset.c @@ -8,8 +8,7 @@ //===----------------------------------------------------------------------===// #include <stdlib.h> - -void *memset(void * dst, int s, size_t count) { +__attribute__ ((weak)) void *memset(void * dst, int s, size_t count) { volatile char * a = dst; while (count-- > 0) *a++ = s; diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile index e6a7ad72..eca63169 100755 --- a/runtime/klee-libc/Makefile +++ b/runtime/klee-libc/Makefile @@ -10,11 +10,13 @@ LEVEL=../.. LIBRARYNAME=klee-libc -DONT_BUILD_RELINKED=1 +MODULE_NAME=klee-libc +#DONT_BUILD_RELINKED=1 BYTECODE_LIBRARY=1 +MODULE_NAME=klee-libc # Don't strip debug info from the module. DEBUG_RUNTIME=1 -NO_PEDANTIC=1 +#NO_PEDANTIC=1 # Add __NO_INLINE__ to prevent glibc from using inline definitions of some # builtins. |