diff options
Diffstat (limited to 'runtime/klee-libc/Makefile.cmake.bitcode')
-rw-r--r-- | runtime/klee-libc/Makefile.cmake.bitcode | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/runtime/klee-libc/Makefile.cmake.bitcode b/runtime/klee-libc/Makefile.cmake.bitcode new file mode 100644 index 00000000..6e85952c --- /dev/null +++ b/runtime/klee-libc/Makefile.cmake.bitcode @@ -0,0 +1,24 @@ +#===--------------------------------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +LEVEL := ../ + +include $(LEVEL)/Makefile.cmake.bitcode.config + +# Prevent glibc from inlining some definitions +# of builtins +LLVMCC.Flags += -D__NO_INLINE__ + +# FIXME: This is a horrible hack +ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1) + MODULE_NAME=klee-libc +else + ARCHIVE_NAME=klee-libc +endif + +include $(LEVEL)/Makefile.cmake.bitcode.rules |