klee-uclibc detection is now a lot cleaner. KLEE now assumes

it can find klee-uclibc inside the same folder as the other
runtime libraries with the name "klee-uclibc.bca"

This is implemented as follows:

* When building, a sym-link is created to klee-uclibc's libc.a file
  in the same directory that the rest of KLEE's runtime libraries
  are built. This done so that if a developer changes klee-uclibc
  on their system then the correct version of klee-uclibc is used
  by KLEE.

* When installing, klee-uclibc's libc.a file is installed in the same
  directory that the rest of KLEE's runtime libraries are installed.

In addition the configure script argument --with-uclibc can now
operate in two ways. It can either be passed the path to the root
of klee-uclibc or it can be passed a path to the libc.a file built
by klee-uclibc. This new behaviour has been added to allow users
to potential use pre-built versions of klee-uclibc.

2 files changed, 57 insertions, 0 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index 24824d08..7eb02d3f 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -23,4 +23,8 @@ ifeq ($(ENABLE_POSIX_RUNTIME),1)
 PARALLEL_DIRS += POSIX
 endif
 
+ifeq ($(ENABLE_UCLIBC),1)
+PARALLEL_DIRS += klee-uclibc
+endif
+
 include $(LEVEL)/Makefile.common
diff --git a/runtime/klee-uclibc/Makefile b/runtime/klee-uclibc/Makefile
new file mode 100644
index 00000000..1e848264
--- /dev/null
+++ b/runtime/klee-uclibc/Makefile
@@ -0,0 +1,53 @@
+#===-- runtime/klee-uclibc/Makefile --------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+# Note klee-uclibc does not really live here.  This makefile just manages the
+# location of the klee-uclibc bitcode archive when building and when installing
+# KLEE.
+
+LEVEL=../..
+
+# We're not really building a bytecode library here
+# but we need to set this so that $(BuildMode) is
+# set appropriately
+BYTECODE_LIBRARY=1
+
+include $(LEVEL)/Makefile.common
+
+# The purpose of setting up this symbolic link is
+# so that KLEE can always look for klee-uclibc
+# in the same place it looks for all the other
+# run time libraries
+uclibc_symlink:=$(PROJ_OBJ_ROOT)/$(BuildMode)/lib/$(KLEE_UCLIBC_BCA_NAME)
+#
+# Force our extra rules to run
+all-local:: $(uclibc_symlink)
+
+$(uclibc_symlink):
+	@echo "Setting up symbolic link to klee-uclibc"
+	$(Verb) ln -s -f $(KLEE_UCLIBC_BCA) $(uclibc_symlink)
+
+# The reasons for copying over klee-uclibc on install are
+#
+# * KLEE can look for klee-uclibc in the same place it looks for all other run
+#   time libraries. 
+# * KLEE can be more easily distributed with klee-uclibc
+
+install:: copy_klee_uclibc
+uninstall:: remove_klee_uclibc
+
+.PHONY: copy_klee_uclibc remove_klee_uclibc
+
+copy_klee_uclibc:
+	@echo "Installing klee-uclibc archive"
+	$(Verb) $(CP) $(KLEE_UCLIBC_BCA) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME)
+
+remove_klee_uclibc:
+	@echo "Removing klee-uclibc archive"
+	$(Verb) $(RM) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME)