about summary refs log tree commit diff homepage
path: root/runtime/Intrinsic
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/Intrinsic')
-rw-r--r--runtime/Intrinsic/Makefile15
-rw-r--r--runtime/Intrinsic/klee_int.c2
2 files changed, 13 insertions, 4 deletions
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/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c
index 56f0f9dc..6ea1e02e 100644
--- a/runtime/Intrinsic/klee_int.c
+++ b/runtime/Intrinsic/klee_int.c
@@ -8,7 +8,7 @@
 //===----------------------------------------------------------------------===//
 
 #include <assert.h>
-#include <klee/klee.h>
+#include "klee/klee.h"
 
 int klee_int(const char *name) {
   int x;