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 | ||||
-rw-r--r-- | runtime/POSIX/fd_32.c | 14 | ||||
-rw-r--r-- | runtime/POSIX/fd_64.c | 13 | ||||
-rwxr-xr-x | runtime/klee-libc/Makefile | 6 |
8 files changed, 36 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/POSIX/fd_32.c b/runtime/POSIX/fd_32.c index 6246f057..1e96de37 100644 --- a/runtime/POSIX/fd_32.c +++ b/runtime/POSIX/fd_32.c @@ -6,7 +6,19 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// +// Contains 32bit definitions of posix file functions +//===--- +#if __GNUC__ +#if __x86_64__ || __ppc64__ +#define ENV64 +#else +#define ENV32 +#endif +#endif + +#include "klee/Config/Version.h" +#if defined(ENV32) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 3)) #define _LARGEFILE64_SOURCE #include "fd.h" @@ -189,3 +201,5 @@ __attribute__((weak)) int lstat64(const char *path, struct stat64 *buf) { __attribute__((weak)) int fstat64(int fd, struct stat64 *buf) { return __fd_fstat(fd, buf); } + +#endif diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c index d0710caf..268579c0 100644 --- a/runtime/POSIX/fd_64.c +++ b/runtime/POSIX/fd_64.c @@ -7,6 +7,17 @@ // //===----------------------------------------------------------------------===// +#if __GNUC__ +#if __x86_64__ || __ppc64__ +#define ENV64 +#else +#define ENV32 +#endif +#endif + + +#include "klee/Config/Version.h" +#if defined(ENV64) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 3)) #define _LARGEFILE64_SOURCE #define _FILE_OFFSET_BITS 64 #include "fd.h" @@ -88,3 +99,5 @@ int getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) { } int __getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) __attribute__((alias("getdents64"))); + +#endif 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. |