diff options
Diffstat (limited to 'runtime/svcomp64/Makefile')
| -rw-r--r-- | runtime/svcomp64/Makefile | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/runtime/svcomp64/Makefile b/runtime/svcomp64/Makefile new file mode 100644 index 00000000..40d44ec3 --- /dev/null +++ b/runtime/svcomp64/Makefile @@ -0,0 +1,32 @@ +#===-- runtime/Intrinsic/Makefile --------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +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=kleeSVCOMPRuntime64 +else +# KLEE built against older versions of LLVM expects a library archive instead +BYTECODE_LIBRARY=1 +LIBRARYNAME=kleeSVCOMPRuntime64 +endif + +DONT_BUILD_RELINKED=1 +# Don't strip debug info from the module. +DEBUG_RUNTIME=1 +NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 + +C.Flags += -fno-builtin -m64 + +include $(LEVEL)/Makefile.common |