From 91f389ab46fb29656600a11a373a54ddf896d821 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 25 Apr 2015 19:48:22 +0100
Subject: Clean up the installation/building of the runtime libraries.

* We don't need to build the native versions so that is now disabled
* We don't need to install (and hence build) the bytecode archive
  library versions of klee-libc or kleeRuntimeIntrinsic for new versions
  of LLVM right now (this is kind of messy).
---
 runtime/Intrinsic/Makefile | 15 ++++++++++++---
 runtime/POSIX/Makefile     |  2 +-
 runtime/klee-libc/Makefile | 15 ++++++++++++---
 3 files changed, 25 insertions(+), 7 deletions(-)

(limited to 'runtime')

diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile
index 3c6b01b3..49f8f9cc 100644
--- a/runtime/Intrinsic/Makefile
+++ b/runtime/Intrinsic/Makefile
@@ -9,15 +9,24 @@
 
 LEVEL=../..
 
+# Needed for LLVM version
+include $(LEVEL)/Makefile.config
+
+ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True)
+# For these versions of LLVM KLEE expects kleeRuntimeIntrinsic to be a LLVM module rather than an archive
+MODULE_NAME=kleeRuntimeIntrinsic
+else
+# KLEE built against older versions of LLVM expects a library archive instead
+BYTECODE_LIBRARY=1
 LIBRARYNAME=kleeRuntimeIntrinsic
+endif
+
 DONT_BUILD_RELINKED=1
-BUILD_ARCHIVE=1
-BYTECODE_LIBRARY=1
 # Don't strip debug info from the module.
 DEBUG_RUNTIME=1
 NO_PEDANTIC=1
+NO_BUILD_ARCHIVE=1
 
-MODULE_NAME=kleeRuntimeIntrinsic
 C.Flags += -fno-builtin
 
 include $(LEVEL)/Makefile.common
diff --git a/runtime/POSIX/Makefile b/runtime/POSIX/Makefile
index 9a42f5c0..1e570098 100644
--- a/runtime/POSIX/Makefile
+++ b/runtime/POSIX/Makefile
@@ -11,10 +11,10 @@ LEVEL=../..
 
 LIBRARYNAME=kleeRuntimePOSIX
 DONT_BUILD_RELINKED=1
-BUILD_ARCHIVE=1
 BYTECODE_LIBRARY=1
 # Don't strip debug info from the module.
 DEBUG_RUNTIME=1
 NO_PEDANTIC=1
+NO_BUILD_ARCHIVE=1
 
 include $(LEVEL)/Makefile.common
diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile
index eca63169..d059ba8a 100755
--- a/runtime/klee-libc/Makefile
+++ b/runtime/klee-libc/Makefile
@@ -9,14 +9,23 @@
 
 LEVEL=../..
 
-LIBRARYNAME=klee-libc
+# Needed for LLVM version
+include $(LEVEL)/Makefile.config
+
+ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True)
+# For these versions of LLVM KLEE expects klee-libc to be a LLVM module rather than an archive
 MODULE_NAME=klee-libc
-#DONT_BUILD_RELINKED=1
+else
+# KLEE built against older versions of LLVM expect a library archive instead
 BYTECODE_LIBRARY=1
-MODULE_NAME=klee-libc
+LIBRARYNAME=klee-libc
+endif
+
+#DONT_BUILD_RELINKED=1
 # Don't strip debug info from the module.
 DEBUG_RUNTIME=1
 #NO_PEDANTIC=1
+NO_BUILD_ARCHIVE=1
 
 # Add __NO_INLINE__ to prevent glibc from using inline definitions of some
 # builtins.
-- 
cgit 1.4.1