aboutsummaryrefslogtreecommitdiffhomepage
path: root/runtime
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2013-08-13 12:22:36 +0200
committerMartin Nowack <martin.nowack@gmail.com>2013-08-27 23:16:18 +0200
commitb1b96a784632f71928220117624a2c07ab3ca9e6 (patch)
tree8b47a50e639521fee563d276579f60e8512f048f /runtime
parentc4147c2ad9ba1e74642e1a3de31be8f4446cc7f3 (diff)
downloadklee-b1b96a784632f71928220117624a2c07ab3ca9e6.tar.gz
Port to LLVM 3.3
Major changes are: - Switching to llvm-link to build archive files - Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847) - intrinsic library functions like memcpy/mov/set use weak linkage to be replaced by e.g. uclibc functions - rewrote linking with library - enhanced MemoryLimit test case to check if mallocs were successful
Diffstat (limited to 'runtime')
-rw-r--r--runtime/Intrinsic/Makefile1
-rw-r--r--runtime/Intrinsic/memcpy.c2
-rw-r--r--runtime/Intrinsic/memmove.c2
-rw-r--r--runtime/Intrinsic/mempcpy.c3
-rw-r--r--runtime/Intrinsic/memset.c3
-rwxr-xr-xruntime/klee-libc/Makefile6
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.