about summary refs log tree commit diff homepage
path: root/runtime/klee-libc
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/klee-libc')
-rw-r--r--runtime/klee-libc/CMakeLists.txt49
-rw-r--r--runtime/klee-libc/Makefile.cmake.bitcode19
2 files changed, 49 insertions, 19 deletions
diff --git a/runtime/klee-libc/CMakeLists.txt b/runtime/klee-libc/CMakeLists.txt
new file mode 100644
index 00000000..653ebb5a
--- /dev/null
+++ b/runtime/klee-libc/CMakeLists.txt
@@ -0,0 +1,49 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+set(LIB_PREFIX "RuntimeKLEELibc")
+set(SRC_FILES
+        __cxa_atexit.c
+        abort.c
+        atexit.c
+        atoi.c
+        bcmp.c
+        calloc.c
+        htonl.c
+        memchr.c
+        mempcpy.c
+        putchar.c
+        stpcpy.c
+        strcat.c
+        strchr.c
+        strcmp.c
+        strcoll.c
+        strcpy.c
+        strlen.c
+        strncmp.c
+        strncpy.c
+        strrchr.c
+        strtol.c
+        strtoul.c
+        tolower.c
+        toupper.c
+        )
+
+# Add __NO_INLINE__ to prevent glibc from using inline definitions of some
+# builtins (i.e. putchar and atoi).
+set(ADDITIONAL_CC_FLAGS
+        -D__NO_INLINE__
+        -std=gnu89
+        )
+
+# Build it
+include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake")
+prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files)
+
+add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "${ADDITIONAL_CC_FLAGS}" "")
\ No newline at end of file
diff --git a/runtime/klee-libc/Makefile.cmake.bitcode b/runtime/klee-libc/Makefile.cmake.bitcode
deleted file mode 100644
index 9902e558..00000000
--- a/runtime/klee-libc/Makefile.cmake.bitcode
+++ /dev/null
@@ -1,19 +0,0 @@
-#===--------------------------------------------------------*- 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__
-
-ARCHIVE_NAME=klee-libc
-
-include $(LEVEL)/Makefile.cmake.bitcode.rules