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.

1 files changed, 27 insertions, 21 deletions

diff --git a/configure b/configure
index 6eda1243..85e7fec2 100755
--- a/configure
+++ b/configure
@@ -649,8 +649,8 @@ RUNTIME_DEBUG_SYMBOLS
 RUNTIME_DISABLE_ASSERTIONS
 RUNTIME_ENABLE_OPTIMIZED
 ENABLE_POSIX_RUNTIME
+KLEE_UCLIBC_BCA
 ENABLE_UCLIBC
-KLEE_UCLIBC
 KLEE_BITCODE_CXX_COMPILER
 KLEE_BITCODE_C_COMPILER
 clang_cxx
@@ -1374,6 +1374,7 @@ Optional Packages:
                           (Default: auto-detect). If set, --with-llvmcc= must
                           be set too.
   --with-uclibc           Enable use of the klee uclibc at the given path
+                          (klee-uclibc root directory or libc.a file
   --with-runtime          Select build configuration for runtime libraries
                           (default [Release+Asserts])
   --with-stp              Location of STP installation directory
@@ -2991,43 +2992,48 @@ if test "${with_uclibc+set}" = set; then :
 fi
 
 
-if (test X${with_uclibc} = X && test -d uclibc); then
-   with_uclibc=uclibc
-fi
-
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking uclibc" >&5
 $as_echo_n "checking uclibc... " >&6; }
 if (test X${with_uclibc} != X); then
-   if test ! -d ${with_uclibc}; then
-       as_fn_error $? "invalid uclibc directory: ${with_uclibc}" "$LINENO" 5
-   fi
+   if test  -d ${with_uclibc}; then
 
-      with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`
+            with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`
 
-   { $as_echo "$as_me:${as_lineno-$LINENO}: result: $with_uclibc" >&5
-$as_echo "$with_uclibc" >&6; }
-else
-   { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
+            KLEE_UCLIBC_BCA="${with_uclibc}/lib/libc.a"
 
+      if test ! -e "${KLEE_UCLIBC_BCA}"; then
+      as_fn_error $? "Could not find file ${KLEE_UCLIBC_BCA}" "$LINENO" 5
+      fi
+   elif test -f ${with_uclibc}; then
+
+            _kud=`dirname ${with_uclibc}`
+      _kud=`cd ${_kud}; pwd 2> /dev/null`
+      _kuf=`basename ${with_uclibc}`
+
+      KLEE_UCLIBC_BCA="${_kud}/${_kuf}"
+   else
+      as_fn_error $? "Could not detect klee-uclibc" "$LINENO" 5
+   fi
 
-cat >>confdefs.h <<_ACEOF
-#define KLEE_UCLIBC "$with_uclibc"
-_ACEOF
 
+   { $as_echo "$as_me:${as_lineno-$LINENO}: result: $KLEE_UCLIBC_BCA" >&5
+$as_echo "$KLEE_UCLIBC_BCA" >&6; }
+   ENABLE_UCLIBC=1
 
 
-if test X${with_uclibc} != X ; then
-  ENABLE_UCLIBC=1
+
+$as_echo "#define SUPPORT_KLEE_UCLIBC 1" >>confdefs.h
 
 else
-  ENABLE_UCLIBC=0
+   { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+   ENABLE_UCLIBC=0
 
 fi
 
 
+
 # Check whether --enable-posix-runtime was given.
 if test "${enable_posix_runtime+set}" = set; then :
   enableval=$enable_posix_runtime;