diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 395 |
1 files changed, 395 insertions, 0 deletions
diff --git a/configure b/configure index 19332245..ab148c2c 100755 --- a/configure +++ b/configure @@ -625,6 +625,8 @@ ac_includes_default="\ ac_subst_vars='LTLIBOBJS LIBOBJS RUNTEST +METASMT_ROOT +ENABLE_METASMT STP_ROOT CXXCPP ac_ct_CXX @@ -642,11 +644,18 @@ LDFLAGS CFLAGS CC RUNTIME_CONFIGURATION +RUNTIME_DEBUG_SYMBOLS RUNTIME_DISABLE_ASSERTIONS RUNTIME_ENABLE_OPTIMIZED ENABLE_POSIX_RUNTIME ENABLE_UCLIBC KLEE_UCLIBC +KLEE_BITCODE_CXX_COMPILER +KLEE_BITCODE_C_COMPILER +clang_cxx +clang +llvm_gxx +llvm_gcc LLVM_BUILD_MODE REQUIRES_RTTI LLVM_IS_RELEASE @@ -711,10 +720,13 @@ with_llvmsrc with_llvmobj with_llvm with_llvm_build_mode +with_llvmcc +with_llvmcxx with_uclibc enable_posix_runtime with_runtime with_stp +with_metasmt ' ac_precious_vars='build_alias host_alias @@ -1353,10 +1365,17 @@ Optional Packages: --with-llvm Location of LLVM Source and Object code --with-llvm-build-mode LLVM build mode (e.g. Debug or Release, default autodetect) + --with-llvmcc Set the path to the C LLVM bitcode compiler to use + (Default: auto-detect). If set, --with-llvmcxx= must + be set too. + --with-llvmcxx Set the path to the C++ LLVM bitcode compiler to use + (Default: auto-detect). If set, --with-llvmcc= must + be set too. --with-uclibc Enable use of the klee uclibc at the given path --with-runtime Select build configuration for runtime libraries (default [Release+Asserts]) --with-stp Location of STP installation directory + --with-metasmt Location of metaSMT installation directory Some influential environment variables: CC C compiler command @@ -2662,6 +2681,306 @@ LLVM_BUILD_MODE=$llvm_build_mode +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking LLVM Bitcode compiler" >&5 +$as_echo_n "checking LLVM Bitcode compiler... " >&6; } +klee_llvm_bc_c_compiler="" +klee_llvm_bc_cxx_compiler="" + + +# Check whether --with-llvmcc was given. +if test "${with_llvmcc+set}" = set; then : + withval=$with_llvmcc; +else + with_llvmcc=none + +fi + + + +# Check whether --with-llvmcxx was given. +if test "${with_llvmcxx+set}" = set; then : + withval=$with_llvmcxx; +else + with_llvmcxx=none + +fi + +if test \( "X$with_llvmcc" != Xnone -a "X$with_llvmcxx" = Xnone \) -o \( "X$with_llvmcxx" != Xnone -a "X$with_llvmcc" = Xnone \) ; then + as_fn_error $? "You must set both --with-llvmcc= and --with-llvmcxx= or set neither" "$LINENO" 5 +fi + +if test X$with_llvmcc = Xnone ; then + + if test -x "$llvm_obj/$llvm_build_mode/bin/clang" ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Found clang in LLVM Build" >&5 +$as_echo "Found clang in LLVM Build" >&6; } + klee_llvm_bc_c_compiler="$llvm_obj/$llvm_build_mode/bin/clang" + + if test -x "$llvm_obj/$llvm_build_mode/bin/clang++" ; then + klee_llvm_bc_cxx_compiler="$llvm_obj/$llvm_build_mode/bin/clang++" + else + as_fn_error $? "Found clang but could not find clang++" "$LINENO" 5 + fi + fi + + if test "X${klee_llvm_bc_c_compiler}" = X ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: " >&5 +$as_echo "" >&6; } # Force a new line + # Extract the first word of "llvm-gcc", so it can be a program name with args. +set dummy llvm-gcc; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_llvm_gcc+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$llvm_gcc"; then + ac_cv_prog_llvm_gcc="$llvm_gcc" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_llvm_gcc="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_llvm_gcc" && ac_cv_prog_llvm_gcc="NOT_FOUND" +fi +fi +llvm_gcc=$ac_cv_prog_llvm_gcc +if test -n "$llvm_gcc"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $llvm_gcc" >&5 +$as_echo "$llvm_gcc" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${llvm_gcc} = FOUND ; then + klee_llvm_bc_c_compiler=`which llvm-gcc` + + # Extract the first word of "llvm-g++", so it can be a program name with args. +set dummy llvm-g++; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_llvm_gxx+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$llvm_gxx"; then + ac_cv_prog_llvm_gxx="$llvm_gxx" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_llvm_gxx="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_llvm_gxx" && ac_cv_prog_llvm_gxx="NOT_FOUND" +fi +fi +llvm_gxx=$ac_cv_prog_llvm_gxx +if test -n "$llvm_gxx"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $llvm_gxx" >&5 +$as_echo "$llvm_gxx" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${llvm_gxx} = FOUND; then + klee_llvm_bc_cxx_compiler=`which llvm-g++` + else + as_fn_error $? "Found llvm-gcc but could not find llvm-g++ in PATH" "$LINENO" 5 + fi + fi + + fi + + if test "X${klee_llvm_bc_c_compiler}" = X ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: " >&5 +$as_echo "" >&6; } # Force a new line + # Extract the first word of "clang", so it can be a program name with args. +set dummy clang; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_clang+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$clang"; then + ac_cv_prog_clang="$clang" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_clang="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_clang" && ac_cv_prog_clang="NOT_FOUND" +fi +fi +clang=$ac_cv_prog_clang +if test -n "$clang"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $clang" >&5 +$as_echo "$clang" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${clang} = FOUND ; then + klee_llvm_bc_c_compiler=`which clang` + + # Extract the first word of "clang++", so it can be a program name with args. +set dummy clang++; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_clang_cxx+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$clang_cxx"; then + ac_cv_prog_clang_cxx="$clang_cxx" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_clang_cxx="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_clang_cxx" && ac_cv_prog_clang_cxx="NOT_FOUND" +fi +fi +clang_cxx=$ac_cv_prog_clang_cxx +if test -n "$clang_cxx"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $clang_cxx" >&5 +$as_echo "$clang_cxx" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${clang_cxx} = FOUND; then + klee_llvm_bc_cxx_compiler=`which clang++` + else + as_fn_error $? "Found clang but could not find clang++ in PATH" "$LINENO" 5 + fi + fi + + fi + + if test X"${klee_llvm_bc_c_compiler}" = X ; then + as_fn_error $? "Could not find a C LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?" "$LINENO" 5 + fi + + if test X"${klee_llvm_bc_cxx_compiler}" = X ; then + as_fn_error $? "Could not find a C++ LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?" "$LINENO" 5 + fi + +else + klee_llvm_bc_c_compiler="$with_llvmcc" + klee_llvm_bc_cxx_compiler="$with_llvmcxx" + + if test \! -x "${klee_llvm_bc_c_compiler}"; then + as_fn_error $? "--with-llvmcc= supplied compiler does not exist" "$LINENO" 5 + fi + + if test \! -x "${klee_llvm_bc_cxx_compiler}"; then + as_fn_error $? "--with-llvmcxx= supplied compiler does not exist" "$LINENO" 5 + fi + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Using user supplied LLVM bitcode compilers." >&5 +$as_echo "Using user supplied LLVM bitcode compilers." >&6; } +fi + +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: Using C llvm compiler : $klee_llvm_bc_c_compiler" >&5 +$as_echo "Using C llvm compiler : $klee_llvm_bc_c_compiler" >&6; } +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: Using C++ llvm compiler : $klee_llvm_bc_cxx_compiler" >&5 +$as_echo "Using C++ llvm compiler : $klee_llvm_bc_cxx_compiler" >&6; } + + +function klee_check_bc() +{ + { $as_echo "$as_me:${as_lineno-$LINENO}: checking ${3} LLVM Bitcode compiler works" >&5 +$as_echo_n "checking ${3} LLVM Bitcode compiler works... " >&6; } + klee_bc_test_file="./.klee_llvm_bitcode_test.${2}" + + echo "int main() { return 0;}" > "${klee_bc_test_file}" + "${1}" -emit-llvm -c "${klee_bc_test_file}" -o "${klee_bc_test_file}.bc" + if test $? -ne 0 ; then + as_fn_error $? "Failed running ${3} LLVM Bitcode compiler" "$LINENO" 5 + fi + + if test \! -e "${klee_bc_test_file}.bc"; then + as_fn_error $? " ${3} LLVM Bitcode compiler did not produce any output" "$LINENO" 5 + fi + + if test -x "$llvm_obj/$llvm_build_mode/bin/llvm-dis" ; then + "$llvm_obj/$llvm_build_mode/bin/llvm-dis" -o "${klee_bc_test_file}.ll" "${klee_bc_test_file}.bc" + + if test $? -ne 0; then + as_fn_error $? "Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?" "$LINENO" 5 + fi + + if test -e "${klee_bc_test_file}.ll" ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Success" >&5 +$as_echo "Success" >&6; } + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" + else + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" + as_fn_error $? "Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?" "$LINENO" 5 + fi + + else + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" + as_fn_error $? "Could not find llvm-dis" "$LINENO" 5 + fi +} + +klee_check_bc "${klee_llvm_bc_c_compiler}" "c" "C" +klee_check_bc "${klee_llvm_bc_cxx_compiler}" "cpp" "CXX" + +KLEE_BITCODE_C_COMPILER=$klee_llvm_bc_c_compiler + +KLEE_BITCODE_CXX_COMPILER=$klee_llvm_bc_cxx_compiler + + + # Check whether --with-uclibc was given. if test "${with_uclibc+set}" = set; then : @@ -2771,6 +3090,8 @@ $as_echo "Release" >&6; } RUNTIME_DISABLE_ASSERTIONS=1 + RUNTIME_DEBUG_SYMBOLS= + elif test X${with_runtime} = XRelease+Asserts; then { $as_echo "$as_me:${as_lineno-$LINENO}: result: Release+Asserts" >&5 $as_echo "Release+Asserts" >&6; } @@ -2778,6 +3099,8 @@ $as_echo "Release+Asserts" >&6; } RUNTIME_DISABLE_ASSERTIONS=0 + RUNTIME_DEBUG_SYMBOLS= + elif test X${with_runtime} = XDebug; then { $as_echo "$as_me:${as_lineno-$LINENO}: result: Debug" >&5 $as_echo "Debug" >&6; } @@ -2785,6 +3108,8 @@ $as_echo "Debug" >&6; } RUNTIME_DISABLE_ASSERTIONS=1 + RUNTIME_DEBUG_SYMBOLS=1 + elif test X${with_runtime} = XDebug+Asserts; then { $as_echo "$as_me:${as_lineno-$LINENO}: result: Debug+Asserts" >&5 $as_echo "Debug+Asserts" >&6; } @@ -2792,6 +3117,8 @@ $as_echo "Debug+Asserts" >&6; } RUNTIME_DISABLE_ASSERTIONS=0 + RUNTIME_DEBUG_SYMBOLS=1 + else as_fn_error $? "invalid configuration: ${with_runtime}" "$LINENO" 5 fi @@ -4590,6 +4917,74 @@ fi fi + + +# Check whether --with-metasmt was given. +if test "${with_metasmt+set}" = set; then : + withval=$with_metasmt; +fi + + +if test X$with_metasmt = X ; then + ENABLE_METASMT=0 + +else + metasmt_root=`cd $with_metasmt 2> /dev/null; pwd` + + old_CPPFLAGS="$CPPFLAGS" + old_LDFLAGS="$LDFLAGS" + CPPFLAGS="$CPPFLAGS -I$metasmt_root/include" + LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT" + for ac_header in $metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp +do : + as_ac_Header=`$as_echo "ac_cv_header_$ac_header" | $as_tr_sh` +ac_fn_cxx_check_header_mongrel "$LINENO" "$ac_header" "$as_ac_Header" "$ac_includes_default" +if eval test \"x\$"$as_ac_Header"\" = x"yes"; then : + cat >>confdefs.h <<_ACEOF +#define `$as_echo "HAVE_$ac_header" | $as_tr_cpp` 1 +_ACEOF + +else + + as_fn_error $? "Unable to use $metasmt_root/include/metaSMT/DirectSolver_Context.hpp header" "$LINENO" 5 + +fi + +done + + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ +#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp +int +main () +{ +metaSMT::logic::QF_BV::new_bitvector(3) + ; + return 0; +} +_ACEOF +if ac_fn_cxx_try_link "$LINENO"; then : + +else + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for new_bitvector() in -lmetaSMT" >&5 +$as_echo_n "checking for new_bitvector() in -lmetaSMT... " >&6; } +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext + CPPFLAGS="$old_CPPFLAGS" + LDFLAGS="$old_LDFLAGS" + + +$as_echo "#define SUPPORT_METASMT 1" >>confdefs.h + + ENABLE_METASMT=1 + + METASMT_ROOT=$metasmt_root + + REQUIRES_RTTI=1 + +fi + # Extract the first word of "runtest", so it can be a program name with args. set dummy runtest; ac_word=$2 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 |