diff options
| -rw-r--r-- | .travis.yml | 50 | ||||
| -rwxr-xr-x | .travis/install-llvm-and-runtime-compiler.sh | 13 | ||||
| -rwxr-xr-x | .travis/klee.sh | 16 | ||||
| -rwxr-xr-x | .travis/stp.sh | 17 | ||||
| -rw-r--r-- | Makefile.common | 5 | ||||
| -rw-r--r-- | Makefile.config.in | 2 | ||||
| -rw-r--r-- | autoconf/configure.ac | 35 | ||||
| -rwxr-xr-x | configure | 1484 | ||||
| -rw-r--r-- | lib/Core/Common.cpp | 72 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 38 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 4 | ||||
| -rw-r--r-- | lib/Core/ExecutorUtil.cpp | 3 | ||||
| -rw-r--r-- | lib/Core/ExternalDispatcher.cpp | 9 | ||||
| -rw-r--r-- | lib/Core/Searcher.cpp | 8 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 23 | ||||
| -rw-r--r-- | lib/Module/Checks.cpp | 1 | ||||
| -rw-r--r-- | lib/Module/InstructionInfoTable.cpp | 50 | ||||
| -rw-r--r-- | lib/Module/KModule.cpp | 56 | ||||
| -rw-r--r-- | lib/Module/ModuleUtil.cpp | 15 | ||||
| -rw-r--r-- | lib/Module/Optimize.cpp | 19 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 8 | ||||
| -rw-r--r-- | lib/Support/TreeStream.cpp | 5 | ||||
| -rw-r--r-- | test/CXX/StaticDestructor.cpp | 2 | ||||
| -rw-r--r-- | test/Coverage/ReadArgs.c | 2 | ||||
| -rw-r--r-- | test/Feature/AsmAddresses.c | 25 | ||||
| -rw-r--r-- | test/Feature/SourceMapping.c | 55 | ||||
| -rw-r--r-- | test/Makefile | 5 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 55 |
28 files changed, 1156 insertions, 921 deletions
diff --git a/.travis.yml b/.travis.yml index 2675e3a8..e868493b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,13 +1,20 @@ language: cpp compiler: - - clang + # FIXME: For now, building with Clang is disabled because the STP built with + # it hits an assertion failure during some tests. We should sort this out + # eventually and file the bug against STP or Clang whichever is appropriate, + # but for now it is easier to just reduce the number of configs we test + # anyway. + # - clang + - gcc env: ########################################################################### # Configurations # - # Each line in the "env" section represents a set of environmental variables - # pass to a build. Thus each line represents a different build + # Each line in the "env" section represents a set of environment variables + # passed to a build. Thus each line represents a different build + # configuration. ########################################################################### # Check the matrix of: @@ -17,8 +24,8 @@ env: # with Asserts enabled. # FIXME: Enable when we want to test LLVM3.5 - #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 - #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 + #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 @@ -34,40 +41,51 @@ env: # FIXME: Do Debug+Asserts builds cache: apt before_install: - # Assume Travis image uses Ubuntu 12.04 LTS + ########################################################################### + # Set up the locations to get various packages from + # We assume the Travis image uses Ubuntu 12.04 LTS + ########################################################################### - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list' - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list' - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' + # Needed for CMake - sudo add-apt-repository -y ppa:ubuntu-sdk-team/ppa + # Needed for new libstdc++ and gcc4.8 - sudo add-apt-repository --yes ppa:ubuntu-toolchain-r/test/ - wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add - - # Needed for new libstdc++ and gcc4.8 - sudo apt-get update + ########################################################################### + # Set up out of source build directory + ########################################################################### + - export KLEE_SRC=`pwd` + - cd ../ + - mkdir build + - cd build/ + - export BUILD_DIR=`pwd` + ########################################################################### + # Install stuff + ########################################################################### # FIXME: STP doesn't need everything from Boost! - sudo apt-get install gcc-4.8 g++-4.8 libcap-dev cmake libboost-all-dev # Make gcc4.8 the default gcc version - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 20 - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 20 - - sudo apt-get install llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev clang-3.4 - # Make Clang3.4 the default clang version (for building KLEE) + # Make Clang3.4 the default clang version + - sudo apt-get install clang-3.4 - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.4 20 - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.4 20 + # Install LLVM and the LLVM bitcode compiler we require to build KLEE + - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh # Install lit (llvm-lit is not available) - sudo pip install lit - # Setup out of source build - - export KLEE_SRC=`pwd` - - cd ../ - - mkdir build - - cd build/ - - export BUILD_DIR=`pwd` # Build STP - mkdir stp - cd stp - ${KLEE_SRC}/.travis/stp.sh - cd ../ script: - # Get need utlities/libraries for testing KLEE + # Get needed utlities/libraries for testing KLEE - mkdir test-utils/ - cd test-utils/ - ${KLEE_SRC}/.travis/testing-utils.sh diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh new file mode 100755 index 00000000..6374747e --- /dev/null +++ b/.travis/install-llvm-and-runtime-compiler.sh @@ -0,0 +1,13 @@ +#!/bin/bash -x +set -ev + +sudo apt-get install llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev + +if [ "${LLVM_VERSION}" != "2.9" ]; then + sudo apt-get install llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION} +else + # Get llvm-gcc. We don't bother installing it + wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 + tar -xjf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 + mv llvm-gcc4.2-2.9-x86_64-linux llvm-gcc +fi diff --git a/.travis/klee.sh b/.travis/klee.sh index 6c4ba745..faf3f5f5 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -2,9 +2,6 @@ # Make sure we exit if there is a failure set -e -# Travis doesn't seem to like this in the yaml file so put it here instead -[ "${LLVM_VERSION}" != "2.9" ] && sudo apt-get install llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION} - # Calculate LLVM branch name to retrieve missing files from SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')" @@ -15,11 +12,9 @@ if [ "${LLVM_VERSION}" != "2.9" ]; then KLEE_CC=/usr/bin/clang-${LLVM_VERSION} KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION} else - # Just use pre-built llvm-gcc. - wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 || exit - tar -xjf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 - KLEE_CC=$(pwd)/llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-gcc - KLEE_CXX=$(pwd)/llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-g++ + # Just use pre-built llvm-gcc downloaded earlier + KLEE_CC=${BUILD_DIR}/llvm-gcc/bin/llvm-gcc + KLEE_CXX=${BUILD_DIR}/llvm-gcc/bin/llvm-g++ export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu @@ -67,6 +62,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ ############################################################################### # Testing ############################################################################### +set +e # We want to let all the tests run before we exit ############################################################################### # Unit tests @@ -77,7 +73,6 @@ svn export http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittes ../Makefile.unittest sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ - make unittests \ DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ @@ -94,10 +89,9 @@ make lit.site.cfg \ DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ ENABLE_SHARED=0 -# Running is parallel is broken and there's no point on our "single core" VM anyway set +e # We want to let all the tests run before we exit -lit -v -j1 . +lit -v . RETURN="${RETURN}$?" ############################################################################### diff --git a/.travis/stp.sh b/.travis/stp.sh index 94bbab4d..abc4e566 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -3,6 +3,8 @@ # Make sure we exit if there is a failure set -e +STP_LOG="$(pwd)/stp-build.log" + if [ "${STP_VERSION}" == "UPSTREAM" ]; then git clone --depth 1 git://github.com/stp/stp.git src mkdir build @@ -10,7 +12,10 @@ if [ "${STP_VERSION}" == "UPSTREAM" ]; then # Disabling building of shared libs is a workaround cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF ../src # Don't try to build stp executable, there's an issue with using gcc4.8 with boost libraries built with gcc4.6 - make libstp CopyPublicHeaders + + set +e # Do not exit if build fails because we need to display the log + make libstp CopyPublicHeaders >> "${STP_LOG}" 2>&1 + elif [ "${STP_VERSION}" == "r940" ]; then # Building the old "r940" version that for some reason we love so much! git clone git://github.com/stp/stp.git src_build @@ -33,8 +38,16 @@ elif [ "${STP_VERSION}" == "r940" ]; then export CXX=g++ ./scripts/configure --with-prefix=${BUILD_DIR}/stp/build --with-cryptominisat2 echo "WARNING FORCING GCC TO BE USED TO COMPILE STP" - make OPTIMIZE=-O2 CFLAGS_M32= install + + set +e # Do not exit if build fails because we need to display the log + make OPTIMIZE=-O2 CFLAGS_M32= install >> "${STP_LOG}" 2>&1 else echo "Unsupported STP_VERSION" exit 1 fi + +# Only show build output if something went wrong to keep log output short +if [ $? -ne 0 ]; then + echo "Build error" + cat "${STP_LOG}" +fi diff --git a/Makefile.common b/Makefile.common index e5e3c18a..e6de9f1e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -30,6 +30,11 @@ endif # Needed to build runtime library using clang (gnu89 is the gcc default) C.Flags += -std=gnu89 +# Build using C++11 if requested +ifeq ($(KLEE_USE_CXX11),1) + CXX.Flags += -std=c++11 +endif + # This is filename that KLEE will look for when trying to load klee-uclibc KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca" diff --git a/Makefile.config.in b/Makefile.config.in index a6dcdcaa..c8e2b57f 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -27,6 +27,8 @@ PROJ_OBJ_ROOT := $(subst //,/,@abs_top_builddir@) # Set the root directory of this project's install prefix PROJ_INSTALL_ROOT := @prefix@ +KLEE_USE_CXX11 := @KLEE_USE_CXX11@ + STP_ROOT := @STP_ROOT@ STP_NEEDS_BOOST := @STP_NEEDS_BOOST@ diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 18822396..97bd5eb6 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -32,8 +32,9 @@ AH_TOP([#ifndef KLEE_CONFIG_CONFIG_H #define KLEE_CONFIG_CONFIG_H]) AH_BOTTOM([#endif]) -dnl FIXME: Make out of tree builds work. - +dnl We need to check for the compiler up here to avoid anything else +dnl starting with a different one. +AC_PROG_CXX(g++ clang++ ) AC_LANG([C++]) dnl ************************************************************************** @@ -154,6 +155,36 @@ else fi AC_SUBST(REQUIRES_RTTI,$requires_rtti) +dnl Provide option to use C++11 +AC_ARG_ENABLE([cxx11],[ --enable-cxx11 Build using C++11], [klee_use_cxx11=1], [klee_use_cxx11=0]) + +dnl LLVM >= 3.5 requires C++11 +AC_MSG_CHECKING([if LLVM needs C++11]) +if test '(' $llvm_version_major -eq 3 -a $llvm_version_minor -ge 5 ')' -o '(' $llvm_version_major -gt 3 ')' ; then + klee_use_cxx11=1 + AC_MSG_RESULT([yes]) +else + AC_MSG_RESULT([no]) +fi + +dnl Check if the compiler supports C++11 (this check is taken from LLVM's configure.ac). +if test X${klee_use_cxx11} = X1; then + klee_old_cxxflags="$CXXFLAGS" + CXXFLAGS="$CXXFLAGS -std=c++11" + AC_LINK_IFELSE([AC_LANG_SOURCE([[ +#include <atomic> +std::atomic<float> x(0.0f); +int main() { return (float)x; } +]])], + [AC_MSG_RESULT([yes])], + [AC_MSG_RESULT([no]) + AC_MSG_ERROR([C++11 not supported])]) + CXXFLAGS="$klee_old_cxxflags" +fi + +AC_SUBST(KLEE_USE_CXX11,$klee_use_cxx11) + + AC_ARG_WITH(llvm-build-mode, AS_HELP_STRING([--with-llvm-build-mode], [LLVM build mode (e.g. Debug or Release, default autodetect)]),,[with_llvm_build_mode=check]) diff --git a/configure b/configure index 38404d73..ff3b3536 100755 --- a/configure +++ b/configure @@ -639,6 +639,13 @@ host_alias target_alias LLVM_SRC LLVM_OBJ +CXX +CXXFLAGS +LDFLAGS +CPPFLAGS +ac_ct_CXX +EXEEXT +OBJEXT build build_cpu build_vendor @@ -655,6 +662,7 @@ LLVM_VERSION_MAJOR LLVM_VERSION_MINOR LLVM_IS_RELEASE REQUIRES_RTTI +KLEE_USE_CXX11 LLVM_BUILD_MODE llvm_gcc llvm_gxx @@ -671,18 +679,11 @@ RUNTIME_DEBUG_SYMBOLS RUNTIME_CONFIGURATION CC CFLAGS -LDFLAGS -CPPFLAGS ac_ct_CC -EXEEXT -OBJEXT CPP GREP EGREP HAVE_SELINUX -CXX -CXXFLAGS -ac_ct_CXX CXXCPP UPSTREAM_STP_LINK_FLAGS STP_NEEDS_BOOST @@ -695,14 +696,14 @@ ac_subst_files='' ac_precious_vars='build_alias host_alias target_alias -CC -CFLAGS -LDFLAGS -CPPFLAGS -CPP CXX CXXFLAGS +LDFLAGS +CPPFLAGS CCC +CC +CFLAGS +CPP CXXCPP' @@ -1279,6 +1280,7 @@ if test -n "$ac_init_help"; then Optional Features: --disable-FEATURE do not include FEATURE (same as --enable-FEATURE=no) --enable-FEATURE[=ARG] include FEATURE [ARG=yes] + --enable-cxx11 Build using C++11 --enable-posix-runtime Enable the POSIX runtime Optional Packages: @@ -1303,15 +1305,15 @@ Optional Packages: --with-metasmt Location of metaSMT installation directory Some influential environment variables: - CC C compiler command - CFLAGS C compiler flags + CXX C++ compiler command + CXXFLAGS C++ compiler flags LDFLAGS linker flags, e.g. -L<lib dir> if you have libraries in a nonstandard directory <lib dir> CPPFLAGS C/C++/Objective C preprocessor flags, e.g. -I<include dir> if you have headers in a nonstandard directory <include dir> + CC C compiler command + CFLAGS C compiler flags CPP C preprocessor - CXX C++ compiler command - CXXFLAGS C++ compiler flags CXXCPP C++ preprocessor Use these variables to override the choices made by `configure' or to help @@ -1820,6 +1822,676 @@ ac_config_headers="$ac_config_headers include/klee/Config/config.h" +ac_ext=cpp +ac_cpp='$CXXCPP $CPPFLAGS' +ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' +ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' +ac_compiler_gnu=$ac_cv_cxx_compiler_gnu +if test -z "$CXX"; then + if test -n "$CCC"; then + CXX=$CCC + else + if test -n "$ac_tool_prefix"; then + for ac_prog in g++ clang++ + do + # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args. +set dummy $ac_tool_prefix$ac_prog; ac_word=$2 +{ echo "$as_me:$LINENO: checking for $ac_word" >&5 +echo $ECHO_N "checking for $ac_word... $ECHO_C" >&6; } +if test "${ac_cv_prog_CXX+set}" = set; then + echo $ECHO_N "(cached) $ECHO_C" >&6 +else + if test -n "$CXX"; then + ac_cv_prog_CXX="$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 { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_executable_p "$as_dir/$ac_word$ac_exec_ext"; }; then + ac_cv_prog_CXX="$ac_tool_prefix$ac_prog" + echo "$as_me:$LINENO: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done +done +IFS=$as_save_IFS + +fi +fi +CXX=$ac_cv_prog_CXX +if test -n "$CXX"; then + { echo "$as_me:$LINENO: result: $CXX" >&5 +echo "${ECHO_T}$CXX" >&6; } +else + { echo "$as_me:$LINENO: result: no" >&5 +echo "${ECHO_T}no" >&6; } +fi + + + test -n "$CXX" && break + done +fi +if test -z "$CXX"; then + ac_ct_CXX=$CXX + for ac_prog in g++ clang++ +do + # Extract the first word of "$ac_prog", so it can be a program name with args. +set dummy $ac_prog; ac_word=$2 +{ echo "$as_me:$LINENO: checking for $ac_word" >&5 +echo $ECHO_N "checking for $ac_word... $ECHO_C" >&6; } +if test "${ac_cv_prog_ac_ct_CXX+set}" = set; then + echo $ECHO_N "(cached) $ECHO_C" >&6 +else + if test -n "$ac_ct_CXX"; then + ac_cv_prog_ac_ct_CXX="$ac_ct_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 { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_executable_p "$as_dir/$ac_word$ac_exec_ext"; }; then + ac_cv_prog_ac_ct_CXX="$ac_prog" + echo "$as_me:$LINENO: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done +done +IFS=$as_save_IFS + +fi +fi +ac_ct_CXX=$ac_cv_prog_ac_ct_CXX +if test -n "$ac_ct_CXX"; then + { echo "$as_me:$LINENO: result: $ac_ct_CXX" >&5 +echo "${ECHO_T}$ac_ct_CXX" >&6; } +else + { echo "$as_me:$LINENO: result: no" >&5 +echo "${ECHO_T}no" >&6; } +fi + + + test -n "$ac_ct_CXX" && break +done + + if test "x$ac_ct_CXX" = x; then + CXX="g++" + else + case $cross_compiling:$ac_tool_warned in +yes:) +{ echo "$as_me:$LINENO: WARNING: In the future, Autoconf will not detect cross-tools +whose name does not start with the host triplet. If you think this +configuration is useful to you, please write to autoconf@gnu.org." >&5 +echo "$as_me: WARNING: In the future, Autoconf will not detect cross-tools +whose name does not start with the host triplet. If you think this +configuration is useful to you, please write to autoconf@gnu.org." >&2;} +ac_tool_warned=yes ;; +esac + CXX=$ac_ct_CXX + fi +fi + + fi +fi +# Provide some information about the compiler. +echo "$as_me:$LINENO: checking for C++ compiler version" >&5 +ac_compiler=`set X $ac_compile; echo $2` +{ (ac_try="$ac_compiler --version >&5" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compiler --version >&5") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } +{ (ac_try="$ac_compiler -v >&5" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compiler -v >&5") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } +{ (ac_try="$ac_compiler -V >&5" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compiler -V >&5") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } + +cat >conftest.$ac_ext <<_ACEOF +/* confdefs.h. */ +_ACEOF +cat confdefs.h >>conftest.$ac_ext +cat >>conftest.$ac_ext <<_ACEOF +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +ac_clean_files_save=$ac_clean_files +ac_clean_files="$ac_clean_files a.out a.exe b.out" +# Try to create an executable without -o first, disregard a.out. +# It will help us diagnose broken compilers, and finding out an intuition +# of exeext. +{ echo "$as_me:$LINENO: checking for C++ compiler default output file name" >&5 +echo $ECHO_N "checking for C++ compiler default output file name... $ECHO_C" >&6; } +ac_link_default=`echo "$ac_link" | sed 's/ -o *conftest[^ ]*//'` +# +# List of possible output files, starting from the most likely. +# The algorithm is not robust to junk in `.', hence go to wildcards (a.*) +# only as a last resort. b.out is created by i960 compilers. +ac_files='a_out.exe a.exe conftest.exe a.out conftest a.* conftest.* b.out' +# +# The IRIX 6 linker writes into existing files which may not be +# executable, retaining their permissions. Remove them first so a +# subsequent execution test works. +ac_rmfiles= +for ac_file in $ac_files +do + case $ac_file in + *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.o | *.obj ) ;; + * ) ac_rmfiles="$ac_rmfiles $ac_file";; + esac +done +rm -f $ac_rmfiles + +if { (ac_try="$ac_link_default" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_link_default") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; then + # Autoconf-2.13 could set the ac_cv_exeext variable to `no'. +# So ignore a value of `no', otherwise this would lead to `EXEEXT = no' +# in a Makefile. We should not override ac_cv_exeext if it was cached, +# so that the user can short-circuit this test for compilers unknown to +# Autoconf. +for ac_file in $ac_files +do + test -f "$ac_file" || continue + case $ac_file in + *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.o | *.obj ) + ;; + [ab].out ) + # We found the default executable, but exeext='' is most + # certainly right. + break;; + *.* ) + if test "${ac_cv_exeext+set}" = set && test "$ac_cv_exeext" != no; + then :; else + ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'` + fi + # We set ac_cv_exeext here because the later test for it is not + # safe: cross compilers may not add the suffix if given an `-o' + # argument, so we may need to know it at that point already. + # Even if this section looks crufty: it has the advantage of + # actually working. + break;; + * ) + break;; + esac +done +test "$ac_cv_exeext" = no && ac_cv_exeext= + +else + echo "$as_me: failed program was:" >&5 +sed 's/^/| /' conftest.$ac_ext >&5 + +{ { echo "$as_me:$LINENO: error: C++ compiler cannot create executables +See \`config.log' for more details." >&5 +echo "$as_me: error: C++ compiler cannot create executables +See \`config.log' for more details." >&2;} + { (exit 77); exit 77; }; } +fi + +ac_exeext=$ac_cv_exeext +{ echo "$as_me:$LINENO: result: $ac_file" >&5 +echo "${ECHO_T}$ac_file" >&6; } + +# Check that the compiler produces executables we can run. If not, either +# the compiler is broken, or we cross compile. +{ echo "$as_me:$LINENO: checking whether the C++ compiler works" >&5 +echo $ECHO_N "checking whether the C++ compiler works... $ECHO_C" >&6; } +# FIXME: These cross compiler hacks should be removed for Autoconf 3.0 +# If not cross compiling, check that we can run a simple program. +if test "$cross_compiling" != yes; then + if { ac_try='./$ac_file' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; }; then + cross_compiling=no + else + if test "$cross_compiling" = maybe; then + cross_compiling=yes + else + { { echo "$as_me:$LINENO: error: cannot run C++ compiled programs. +If you meant to cross compile, use \`--host'. +See \`config.log' for more details." >&5 +echo "$as_me: error: cannot run C++ compiled programs. +If you meant to cross compile, use \`--host'. +See \`config.log' for more details." >&2;} + { (exit 1); exit 1; }; } + fi + fi +fi +{ echo "$as_me:$LINENO: result: yes" >&5 +echo "${ECHO_T}yes" >&6; } + +rm -f a.out a.exe conftest$ac_cv_exeext b.out +ac_clean_files=$ac_clean_files_save +# Check that the compiler produces executables we can run. If not, either +# the compiler is broken, or we cross compile. +{ echo "$as_me:$LINENO: checking whether we are cross compiling" >&5 +echo $ECHO_N "checking whether we are cross compiling... $ECHO_C" >&6; } +{ echo "$as_me:$LINENO: result: $cross_compiling" >&5 +echo "${ECHO_T}$cross_compiling" >&6; } + +{ echo "$as_me:$LINENO: checking for suffix of executables" >&5 +echo $ECHO_N "checking for suffix of executables... $ECHO_C" >&6; } +if { (ac_try="$ac_link" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_link") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; then + # If both `conftest.exe' and `conftest' are `present' (well, observable) +# catch `conftest.exe'. For instance with Cygwin, `ls conftest' will +# work properly (i.e., refer to `conftest.exe'), while it won't with +# `rm'. +for ac_file in conftest.exe conftest conftest.*; do + test -f "$ac_file" || continue + case $ac_file in + *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.o | *.obj ) ;; + *.* ) ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'` + break;; + * ) break;; + esac +done +else + { { echo "$as_me:$LINENO: error: cannot compute suffix of executables: cannot compile and link +See \`config.log' for more details." >&5 +echo "$as_me: error: cannot compute suffix of executables: cannot compile and link +See \`config.log' for more details." >&2;} + { (exit 1); exit 1; }; } +fi + +rm -f conftest$ac_cv_exeext +{ echo "$as_me:$LINENO: result: $ac_cv_exeext" >&5 +echo "${ECHO_T}$ac_cv_exeext" >&6; } + +rm -f conftest.$ac_ext +EXEEXT=$ac_cv_exeext +ac_exeext=$EXEEXT +{ echo "$as_me:$LINENO: checking for suffix of object files" >&5 +echo $ECHO_N "checking for suffix of object files... $ECHO_C" >&6; } +if test "${ac_cv_objext+set}" = set; then + echo $ECHO_N "(cached) $ECHO_C" >&6 +else + cat >conftest.$ac_ext <<_ACEOF +/* confdefs.h. */ +_ACEOF +cat confdefs.h >>conftest.$ac_ext +cat >>conftest.$ac_ext <<_ACEOF +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +rm -f conftest.o conftest.obj +if { (ac_try="$ac_compile" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compile") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; then + for ac_file in conftest.o conftest.obj conftest.*; do + test -f "$ac_file" || continue; + case $ac_file in + *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf ) ;; + *) ac_cv_objext=`expr "$ac_file" : '.*\.\(.*\)'` + break;; + esac +done +else + echo "$as_me: failed program was:" >&5 +sed 's/^/| /' conftest.$ac_ext >&5 + +{ { echo "$as_me:$LINENO: error: cannot compute suffix of object files: cannot compile +See \`config.log' for more details." >&5 +echo "$as_me: error: cannot compute suffix of object files: cannot compile +See \`config.log' for more details." >&2;} + { (exit 1); exit 1; }; } +fi + +rm -f conftest.$ac_cv_objext conftest.$ac_ext +fi +{ echo "$as_me:$LINENO: result: $ac_cv_objext" >&5 +echo "${ECHO_T}$ac_cv_objext" >&6; } +OBJEXT=$ac_cv_objext +ac_objext=$OBJEXT +{ echo "$as_me:$LINENO: checking whether we are using the GNU C++ compiler" >&5 +echo $ECHO_N "checking whether we are using the GNU C++ compiler... $ECHO_C" >&6; } +if test "${ac_cv_cxx_compiler_gnu+set}" = set; then + echo $ECHO_N "(cached) $ECHO_C" >&6 +else + cat >conftest.$ac_ext <<_ACEOF +/* confdefs.h. */ +_ACEOF +cat confdefs.h >>conftest.$ac_ext +cat >>conftest.$ac_ext <<_ACEOF +/* end confdefs.h. */ + +int +main () +{ +#ifndef __GNUC__ + choke me +#endif + + ; + return 0; +} +_ACEOF +rm -f conftest.$ac_objext +if { (ac_try="$ac_compile" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compile") 2>conftest.er1 + ac_status=$? + grep -v '^ *+' conftest.er1 >conftest.err + rm -f conftest.er1 + cat conftest.err >&5 + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } && + { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; } && + { ac_try='test -s conftest.$ac_objext' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; }; then + ac_compiler_gnu=yes +else + echo "$as_me: failed program was:" >&5 +sed 's/^/| /' conftest.$ac_ext >&5 + + ac_compiler_gnu=no +fi + +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext +ac_cv_cxx_compiler_gnu=$ac_compiler_gnu + +fi +{ echo "$as_me:$LINENO: result: $ac_cv_cxx_compiler_gnu" >&5 +echo "${ECHO_T}$ac_cv_cxx_compiler_gnu" >&6; } +GXX=`test $ac_compiler_gnu = yes && echo yes` +ac_test_CXXFLAGS=${CXXFLAGS+set} +ac_save_CXXFLAGS=$CXXFLAGS +{ echo "$as_me:$LINENO: checking whether $CXX accepts -g" >&5 +echo $ECHO_N "checking whether $CXX accepts -g... $ECHO_C" >&6; } +if test "${ac_cv_prog_cxx_g+set}" = set; then + echo $ECHO_N "(cached) $ECHO_C" >&6 +else + ac_save_cxx_werror_flag=$ac_cxx_werror_flag + ac_cxx_werror_flag=yes + ac_cv_prog_cxx_g=no + CXXFLAGS="-g" + cat >conftest.$ac_ext <<_ACEOF +/* confdefs.h. */ +_ACEOF +cat confdefs.h >>conftest.$ac_ext +cat >>conftest.$ac_ext <<_ACEOF +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +rm -f conftest.$ac_objext +if { (ac_try="$ac_compile" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compile") 2>conftest.er1 + ac_status=$? + grep -v '^ *+' conftest.er1 >conftest.err + rm -f conftest.er1 + cat conftest.err >&5 + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } && + { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; } && + { ac_try='test -s conftest.$ac_objext' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; }; then + ac_cv_prog_cxx_g=yes +else + echo "$as_me: failed program was:" >&5 +sed 's/^/| /' conftest.$ac_ext >&5 + + CXXFLAGS="" + cat >conftest.$ac_ext <<_ACEOF +/* confdefs.h. */ +_ACEOF +cat confdefs.h >>conftest.$ac_ext +cat >>conftest.$ac_ext <<_ACEOF +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +rm -f conftest.$ac_objext +if { (ac_try="$ac_compile" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compile") 2>conftest.er1 + ac_status=$? + grep -v '^ *+' conftest.er1 >conftest.err + rm -f conftest.er1 + cat conftest.err >&5 + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } && + { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; } && + { ac_try='test -s conftest.$ac_objext' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; }; then + : +else + echo "$as_me: failed program was:" >&5 +sed 's/^/| /' conftest.$ac_ext >&5 + + ac_cxx_werror_flag=$ac_save_cxx_werror_flag + CXXFLAGS="-g" + cat >conftest.$ac_ext <<_ACEOF +/* confdefs.h. */ +_ACEOF +cat confdefs.h >>conftest.$ac_ext +cat >>conftest.$ac_ext <<_ACEOF +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +rm -f conftest.$ac_objext +if { (ac_try="$ac_compile" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_compile") 2>conftest.er1 + ac_status=$? + grep -v '^ *+' conftest.er1 >conftest.err + rm -f conftest.er1 + cat conftest.err >&5 + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } && + { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; } && + { ac_try='test -s conftest.$ac_objext' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; }; then + ac_cv_prog_cxx_g=yes +else + echo "$as_me: failed program was:" >&5 +sed 's/^/| /' conftest.$ac_ext >&5 + + +fi + +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext +fi + +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext +fi + +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext + ac_cxx_werror_flag=$ac_save_cxx_werror_flag +fi +{ echo "$as_me:$LINENO: result: $ac_cv_prog_cxx_g" >&5 +echo "${ECHO_T}$ac_cv_prog_cxx_g" >&6; } +if test "$ac_test_CXXFLAGS" = set; then + CXXFLAGS=$ac_save_CXXFLAGS +elif test $ac_cv_prog_cxx_g = yes; then + if test "$GXX" = yes; then + CXXFLAGS="-g -O2" + else + CXXFLAGS="-g" + fi +else + if test "$GXX" = yes; then + CXXFLAGS="-O2" + else + CXXFLAGS= + fi +fi +ac_ext=c +ac_cpp='$CPP $CPPFLAGS' +ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' +ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' +ac_compiler_gnu=$ac_cv_c_compiler_gnu ac_ext=cpp ac_cpp='$CXXCPP $CPPFLAGS' @@ -2108,6 +2780,97 @@ fi REQUIRES_RTTI=$requires_rtti +# Check whether --enable-cxx11 was given. +if test "${enable_cxx11+set}" = set; then + enableval=$enable_cxx11; klee_use_cxx11=1 +else + klee_use_cxx11=0 +fi + + +{ echo "$as_me:$LINENO: checking if LLVM needs C++11" >&5 +echo $ECHO_N "checking if LLVM needs C++11... $ECHO_C" >&6; } +if test '(' $llvm_version_major -eq 3 -a $llvm_version_minor -ge 5 ')' -o '(' $llvm_version_major -gt 3 ')' ; then + klee_use_cxx11=1 + { echo "$as_me:$LINENO: result: yes" >&5 +echo "${ECHO_T}yes" >&6; } +else + { echo "$as_me:$LINENO: result: no" >&5 +echo "${ECHO_T}no" >&6; } +fi + +if test X${klee_use_cxx11} = X1; then + klee_old_cxxflags="$CXXFLAGS" + CXXFLAGS="$CXXFLAGS -std=c++11" + +cat >conftest.$ac_ext <<_ACEOF +/* confdefs.h. */ +_ACEOF +cat confdefs.h >>conftest.$ac_ext +cat >>conftest.$ac_ext <<_ACEOF +/* end confdefs.h. */ + +#include <atomic> +std::atomic<float> x(0.0f); +int main() { return (float)x; } + +_ACEOF +rm -f conftest.$ac_objext conftest$ac_exeext +if { (ac_try="$ac_link" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_link") 2>conftest.er1 + ac_status=$? + grep -v '^ *+' conftest.er1 >conftest.err + rm -f conftest.er1 + cat conftest.err >&5 + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); } && + { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; } && + { ac_try='test -s conftest$ac_exeext' + { (case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 + (eval "$ac_try") 2>&5 + ac_status=$? + echo "$as_me:$LINENO: \$? = $ac_status" >&5 + (exit $ac_status); }; }; then + { echo "$as_me:$LINENO: result: yes" >&5 +echo "${ECHO_T}yes" >&6; } +else + echo "$as_me: failed program was:" >&5 +sed 's/^/| /' conftest.$ac_ext >&5 + + { echo "$as_me:$LINENO: result: no" >&5 +echo "${ECHO_T}no" >&6; } + { { echo "$as_me:$LINENO: error: C++11 not supported" >&5 +echo "$as_me: error: C++11 not supported" >&2;} + { (exit 1); exit 1; }; } +fi + +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext + CXXFLAGS="$klee_old_cxxflags" +fi + +KLEE_USE_CXX11=$klee_use_cxx11 + + + # Check whether --with-llvm-build-mode was given. if test "${with_llvm_build_mode+set}" = set; then @@ -3013,245 +3776,6 @@ eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 echo "$as_me:$LINENO: \$? = $ac_status" >&5 (exit $ac_status); } -cat >conftest.$ac_ext <<_ACEOF -/* confdefs.h. */ -_ACEOF -cat confdefs.h >>conftest.$ac_ext -cat >>conftest.$ac_ext <<_ACEOF -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -ac_clean_files_save=$ac_clean_files -ac_clean_files="$ac_clean_files a.out a.exe b.out" -# Try to create an executable without -o first, disregard a.out. -# It will help us diagnose broken compilers, and finding out an intuition -# of exeext. -{ echo "$as_me:$LINENO: checking for C compiler default output file name" >&5 -echo $ECHO_N "checking for C compiler default output file name... $ECHO_C" >&6; } -ac_link_default=`echo "$ac_link" | sed 's/ -o *conftest[^ ]*//'` -# -# List of possible output files, starting from the most likely. -# The algorithm is not robust to junk in `.', hence go to wildcards (a.*) -# only as a last resort. b.out is created by i960 compilers. -ac_files='a_out.exe a.exe conftest.exe a.out conftest a.* conftest.* b.out' -# -# The IRIX 6 linker writes into existing files which may not be -# executable, retaining their permissions. Remove them first so a -# subsequent execution test works. -ac_rmfiles= -for ac_file in $ac_files -do - case $ac_file in - *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.o | *.obj ) ;; - * ) ac_rmfiles="$ac_rmfiles $ac_file";; - esac -done -rm -f $ac_rmfiles - -if { (ac_try="$ac_link_default" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_link_default") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; then - # Autoconf-2.13 could set the ac_cv_exeext variable to `no'. -# So ignore a value of `no', otherwise this would lead to `EXEEXT = no' -# in a Makefile. We should not override ac_cv_exeext if it was cached, -# so that the user can short-circuit this test for compilers unknown to -# Autoconf. -for ac_file in $ac_files -do - test -f "$ac_file" || continue - case $ac_file in - *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.o | *.obj ) - ;; - [ab].out ) - # We found the default executable, but exeext='' is most - # certainly right. - break;; - *.* ) - if test "${ac_cv_exeext+set}" = set && test "$ac_cv_exeext" != no; - then :; else - ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'` - fi - # We set ac_cv_exeext here because the later test for it is not - # safe: cross compilers may not add the suffix if given an `-o' - # argument, so we may need to know it at that point already. - # Even if this section looks crufty: it has the advantage of - # actually working. - break;; - * ) - break;; - esac -done -test "$ac_cv_exeext" = no && ac_cv_exeext= - -else - echo "$as_me: failed program was:" >&5 -sed 's/^/| /' conftest.$ac_ext >&5 - -{ { echo "$as_me:$LINENO: error: C compiler cannot create executables -See \`config.log' for more details." >&5 -echo "$as_me: error: C compiler cannot create executables -See \`config.log' for more details." >&2;} - { (exit 77); exit 77; }; } -fi - -ac_exeext=$ac_cv_exeext -{ echo "$as_me:$LINENO: result: $ac_file" >&5 -echo "${ECHO_T}$ac_file" >&6; } - -# Check that the compiler produces executables we can run. If not, either -# the compiler is broken, or we cross compile. -{ echo "$as_me:$LINENO: checking whether the C compiler works" >&5 -echo $ECHO_N "checking whether the C compiler works... $ECHO_C" >&6; } -# FIXME: These cross compiler hacks should be removed for Autoconf 3.0 -# If not cross compiling, check that we can run a simple program. -if test "$cross_compiling" != yes; then - if { ac_try='./$ac_file' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; }; then - cross_compiling=no - else - if test "$cross_compiling" = maybe; then - cross_compiling=yes - else - { { echo "$as_me:$LINENO: error: cannot run C compiled programs. -If you meant to cross compile, use \`--host'. -See \`config.log' for more details." >&5 -echo "$as_me: error: cannot run C compiled programs. -If you meant to cross compile, use \`--host'. -See \`config.log' for more details." >&2;} - { (exit 1); exit 1; }; } - fi - fi -fi -{ echo "$as_me:$LINENO: result: yes" >&5 -echo "${ECHO_T}yes" >&6; } - -rm -f a.out a.exe conftest$ac_cv_exeext b.out -ac_clean_files=$ac_clean_files_save -# Check that the compiler produces executables we can run. If not, either -# the compiler is broken, or we cross compile. -{ echo "$as_me:$LINENO: checking whether we are cross compiling" >&5 -echo $ECHO_N "checking whether we are cross compiling... $ECHO_C" >&6; } -{ echo "$as_me:$LINENO: result: $cross_compiling" >&5 -echo "${ECHO_T}$cross_compiling" >&6; } - -{ echo "$as_me:$LINENO: checking for suffix of executables" >&5 -echo $ECHO_N "checking for suffix of executables... $ECHO_C" >&6; } -if { (ac_try="$ac_link" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_link") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; then - # If both `conftest.exe' and `conftest' are `present' (well, observable) -# catch `conftest.exe'. For instance with Cygwin, `ls conftest' will -# work properly (i.e., refer to `conftest.exe'), while it won't with -# `rm'. -for ac_file in conftest.exe conftest conftest.*; do - test -f "$ac_file" || continue - case $ac_file in - *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.o | *.obj ) ;; - *.* ) ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'` - break;; - * ) break;; - esac -done -else - { { echo "$as_me:$LINENO: error: cannot compute suffix of executables: cannot compile and link -See \`config.log' for more details." >&5 -echo "$as_me: error: cannot compute suffix of executables: cannot compile and link -See \`config.log' for more details." >&2;} - { (exit 1); exit 1; }; } -fi - -rm -f conftest$ac_cv_exeext -{ echo "$as_me:$LINENO: result: $ac_cv_exeext" >&5 -echo "${ECHO_T}$ac_cv_exeext" >&6; } - -rm -f conftest.$ac_ext -EXEEXT=$ac_cv_exeext -ac_exeext=$EXEEXT -{ echo "$as_me:$LINENO: checking for suffix of object files" >&5 -echo $ECHO_N "checking for suffix of object files... $ECHO_C" >&6; } -if test "${ac_cv_objext+set}" = set; then - echo $ECHO_N "(cached) $ECHO_C" >&6 -else - cat >conftest.$ac_ext <<_ACEOF -/* confdefs.h. */ -_ACEOF -cat confdefs.h >>conftest.$ac_ext -cat >>conftest.$ac_ext <<_ACEOF -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -rm -f conftest.o conftest.obj -if { (ac_try="$ac_compile" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compile") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; then - for ac_file in conftest.o conftest.obj conftest.*; do - test -f "$ac_file" || continue; - case $ac_file in - *.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf ) ;; - *) ac_cv_objext=`expr "$ac_file" : '.*\.\(.*\)'` - break;; - esac -done -else - echo "$as_me: failed program was:" >&5 -sed 's/^/| /' conftest.$ac_ext >&5 - -{ { echo "$as_me:$LINENO: error: cannot compute suffix of object files: cannot compile -See \`config.log' for more details." >&5 -echo "$as_me: error: cannot compute suffix of object files: cannot compile -See \`config.log' for more details." >&2;} - { (exit 1); exit 1; }; } -fi - -rm -f conftest.$ac_cv_objext conftest.$ac_ext -fi -{ echo "$as_me:$LINENO: result: $ac_cv_objext" >&5 -echo "${ECHO_T}$ac_cv_objext" >&6; } -OBJEXT=$ac_cv_objext -ac_objext=$OBJEXT { echo "$as_me:$LINENO: checking whether we are using the GNU C compiler" >&5 echo $ECHO_N "checking whether we are using the GNU C compiler... $ECHO_C" >&6; } if test "${ac_cv_c_compiler_gnu+set}" = set; then @@ -4811,439 +5335,6 @@ ac_cpp='$CXXCPP $CPPFLAGS' ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' ac_compiler_gnu=$ac_cv_cxx_compiler_gnu -if test -z "$CXX"; then - if test -n "$CCC"; then - CXX=$CCC - else - if test -n "$ac_tool_prefix"; then - for ac_prog in g++ c++ gpp aCC CC cxx cc++ cl.exe FCC KCC RCC xlC_r xlC - do - # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args. -set dummy $ac_tool_prefix$ac_prog; ac_word=$2 -{ echo "$as_me:$LINENO: checking for $ac_word" >&5 -echo $ECHO_N "checking for $ac_word... $ECHO_C" >&6; } -if test "${ac_cv_prog_CXX+set}" = set; then - echo $ECHO_N "(cached) $ECHO_C" >&6 -else - if test -n "$CXX"; then - ac_cv_prog_CXX="$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 { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_executable_p "$as_dir/$ac_word$ac_exec_ext"; }; then - ac_cv_prog_CXX="$ac_tool_prefix$ac_prog" - echo "$as_me:$LINENO: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done -done -IFS=$as_save_IFS - -fi -fi -CXX=$ac_cv_prog_CXX -if test -n "$CXX"; then - { echo "$as_me:$LINENO: result: $CXX" >&5 -echo "${ECHO_T}$CXX" >&6; } -else - { echo "$as_me:$LINENO: result: no" >&5 -echo "${ECHO_T}no" >&6; } -fi - - - test -n "$CXX" && break - done -fi -if test -z "$CXX"; then - ac_ct_CXX=$CXX - for ac_prog in g++ c++ gpp aCC CC cxx cc++ cl.exe FCC KCC RCC xlC_r xlC -do - # Extract the first word of "$ac_prog", so it can be a program name with args. -set dummy $ac_prog; ac_word=$2 -{ echo "$as_me:$LINENO: checking for $ac_word" >&5 -echo $ECHO_N "checking for $ac_word... $ECHO_C" >&6; } -if test "${ac_cv_prog_ac_ct_CXX+set}" = set; then - echo $ECHO_N "(cached) $ECHO_C" >&6 -else - if test -n "$ac_ct_CXX"; then - ac_cv_prog_ac_ct_CXX="$ac_ct_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 { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_executable_p "$as_dir/$ac_word$ac_exec_ext"; }; then - ac_cv_prog_ac_ct_CXX="$ac_prog" - echo "$as_me:$LINENO: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done -done -IFS=$as_save_IFS - -fi -fi -ac_ct_CXX=$ac_cv_prog_ac_ct_CXX -if test -n "$ac_ct_CXX"; then - { echo "$as_me:$LINENO: result: $ac_ct_CXX" >&5 -echo "${ECHO_T}$ac_ct_CXX" >&6; } -else - { echo "$as_me:$LINENO: result: no" >&5 -echo "${ECHO_T}no" >&6; } -fi - - - test -n "$ac_ct_CXX" && break -done - - if test "x$ac_ct_CXX" = x; then - CXX="g++" - else - case $cross_compiling:$ac_tool_warned in -yes:) -{ echo "$as_me:$LINENO: WARNING: In the future, Autoconf will not detect cross-tools -whose name does not start with the host triplet. If you think this -configuration is useful to you, please write to autoconf@gnu.org." >&5 -echo "$as_me: WARNING: In the future, Autoconf will not detect cross-tools -whose name does not start with the host triplet. If you think this -configuration is useful to you, please write to autoconf@gnu.org." >&2;} -ac_tool_warned=yes ;; -esac - CXX=$ac_ct_CXX - fi -fi - - fi -fi -# Provide some information about the compiler. -echo "$as_me:$LINENO: checking for C++ compiler version" >&5 -ac_compiler=`set X $ac_compile; echo $2` -{ (ac_try="$ac_compiler --version >&5" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compiler --version >&5") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); } -{ (ac_try="$ac_compiler -v >&5" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compiler -v >&5") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); } -{ (ac_try="$ac_compiler -V >&5" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compiler -V >&5") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); } - -{ echo "$as_me:$LINENO: checking whether we are using the GNU C++ compiler" >&5 -echo $ECHO_N "checking whether we are using the GNU C++ compiler... $ECHO_C" >&6; } -if test "${ac_cv_cxx_compiler_gnu+set}" = set; then - echo $ECHO_N "(cached) $ECHO_C" >&6 -else - cat >conftest.$ac_ext <<_ACEOF -/* confdefs.h. */ -_ACEOF -cat confdefs.h >>conftest.$ac_ext -cat >>conftest.$ac_ext <<_ACEOF -/* end confdefs.h. */ - -int -main () -{ -#ifndef __GNUC__ - choke me -#endif - - ; - return 0; -} -_ACEOF -rm -f conftest.$ac_objext -if { (ac_try="$ac_compile" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compile") 2>conftest.er1 - ac_status=$? - grep -v '^ *+' conftest.er1 >conftest.err - rm -f conftest.er1 - cat conftest.err >&5 - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); } && - { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; } && - { ac_try='test -s conftest.$ac_objext' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; }; then - ac_compiler_gnu=yes -else - echo "$as_me: failed program was:" >&5 -sed 's/^/| /' conftest.$ac_ext >&5 - - ac_compiler_gnu=no -fi - -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext -ac_cv_cxx_compiler_gnu=$ac_compiler_gnu - -fi -{ echo "$as_me:$LINENO: result: $ac_cv_cxx_compiler_gnu" >&5 -echo "${ECHO_T}$ac_cv_cxx_compiler_gnu" >&6; } -GXX=`test $ac_compiler_gnu = yes && echo yes` -ac_test_CXXFLAGS=${CXXFLAGS+set} -ac_save_CXXFLAGS=$CXXFLAGS -{ echo "$as_me:$LINENO: checking whether $CXX accepts -g" >&5 -echo $ECHO_N "checking whether $CXX accepts -g... $ECHO_C" >&6; } -if test "${ac_cv_prog_cxx_g+set}" = set; then - echo $ECHO_N "(cached) $ECHO_C" >&6 -else - ac_save_cxx_werror_flag=$ac_cxx_werror_flag - ac_cxx_werror_flag=yes - ac_cv_prog_cxx_g=no - CXXFLAGS="-g" - cat >conftest.$ac_ext <<_ACEOF -/* confdefs.h. */ -_ACEOF -cat confdefs.h >>conftest.$ac_ext -cat >>conftest.$ac_ext <<_ACEOF -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -rm -f conftest.$ac_objext -if { (ac_try="$ac_compile" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compile") 2>conftest.er1 - ac_status=$? - grep -v '^ *+' conftest.er1 >conftest.err - rm -f conftest.er1 - cat conftest.err >&5 - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); } && - { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; } && - { ac_try='test -s conftest.$ac_objext' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; }; then - ac_cv_prog_cxx_g=yes -else - echo "$as_me: failed program was:" >&5 -sed 's/^/| /' conftest.$ac_ext >&5 - - CXXFLAGS="" - cat >conftest.$ac_ext <<_ACEOF -/* confdefs.h. */ -_ACEOF -cat confdefs.h >>conftest.$ac_ext -cat >>conftest.$ac_ext <<_ACEOF -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -rm -f conftest.$ac_objext -if { (ac_try="$ac_compile" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compile") 2>conftest.er1 - ac_status=$? - grep -v '^ *+' conftest.er1 >conftest.err - rm -f conftest.er1 - cat conftest.err >&5 - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); } && - { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; } && - { ac_try='test -s conftest.$ac_objext' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; }; then - : -else - echo "$as_me: failed program was:" >&5 -sed 's/^/| /' conftest.$ac_ext >&5 - - ac_cxx_werror_flag=$ac_save_cxx_werror_flag - CXXFLAGS="-g" - cat >conftest.$ac_ext <<_ACEOF -/* confdefs.h. */ -_ACEOF -cat confdefs.h >>conftest.$ac_ext -cat >>conftest.$ac_ext <<_ACEOF -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -rm -f conftest.$ac_objext -if { (ac_try="$ac_compile" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_compile") 2>conftest.er1 - ac_status=$? - grep -v '^ *+' conftest.er1 >conftest.err - rm -f conftest.er1 - cat conftest.err >&5 - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); } && - { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; } && - { ac_try='test -s conftest.$ac_objext' - { (case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5 - (eval "$ac_try") 2>&5 - ac_status=$? - echo "$as_me:$LINENO: \$? = $ac_status" >&5 - (exit $ac_status); }; }; then - ac_cv_prog_cxx_g=yes -else - echo "$as_me: failed program was:" >&5 -sed 's/^/| /' conftest.$ac_ext >&5 - - -fi - -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext -fi - -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext -fi - -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext - ac_cxx_werror_flag=$ac_save_cxx_werror_flag -fi -{ echo "$as_me:$LINENO: result: $ac_cv_prog_cxx_g" >&5 -echo "${ECHO_T}$ac_cv_prog_cxx_g" >&6; } -if test "$ac_test_CXXFLAGS" = set; then - CXXFLAGS=$ac_save_CXXFLAGS -elif test $ac_cv_prog_cxx_g = yes; then - if test "$GXX" = yes; then - CXXFLAGS="-g -O2" - else - CXXFLAGS="-g" - fi -else - if test "$GXX" = yes; then - CXXFLAGS="-O2" - else - CXXFLAGS= - fi -fi -ac_ext=cpp -ac_cpp='$CXXCPP $CPPFLAGS' -ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' -ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' -ac_compiler_gnu=$ac_cv_cxx_compiler_gnu - - -ac_ext=cpp -ac_cpp='$CXXCPP $CPPFLAGS' -ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' -ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' -ac_compiler_gnu=$ac_cv_cxx_compiler_gnu { echo "$as_me:$LINENO: checking how to run the C++ preprocessor" >&5 echo $ECHO_N "checking how to run the C++ preprocessor... $ECHO_C" >&6; } if test -z "$CXXCPP"; then @@ -7420,6 +7511,13 @@ host_alias!$host_alias$ac_delim target_alias!$target_alias$ac_delim LLVM_SRC!$LLVM_SRC$ac_delim LLVM_OBJ!$LLVM_OBJ$ac_delim +CXX!$CXX$ac_delim +CXXFLAGS!$CXXFLAGS$ac_delim +LDFLAGS!$LDFLAGS$ac_delim +CPPFLAGS!$CPPFLAGS$ac_delim +ac_ct_CXX!$ac_ct_CXX$ac_delim +EXEEXT!$EXEEXT$ac_delim +OBJEXT!$OBJEXT$ac_delim build!$build$ac_delim build_cpu!$build_cpu$ac_delim build_vendor!$build_vendor$ac_delim @@ -7436,6 +7534,7 @@ LLVM_VERSION_MAJOR!$LLVM_VERSION_MAJOR$ac_delim LLVM_VERSION_MINOR!$LLVM_VERSION_MINOR$ac_delim LLVM_IS_RELEASE!$LLVM_IS_RELEASE$ac_delim REQUIRES_RTTI!$REQUIRES_RTTI$ac_delim +KLEE_USE_CXX11!$KLEE_USE_CXX11$ac_delim LLVM_BUILD_MODE!$LLVM_BUILD_MODE$ac_delim llvm_gcc!$llvm_gcc$ac_delim llvm_gxx!$llvm_gxx$ac_delim @@ -7452,18 +7551,11 @@ RUNTIME_DEBUG_SYMBOLS!$RUNTIME_DEBUG_SYMBOLS$ac_delim RUNTIME_CONFIGURATION!$RUNTIME_CONFIGURATION$ac_delim CC!$CC$ac_delim CFLAGS!$CFLAGS$ac_delim -LDFLAGS!$LDFLAGS$ac_delim -CPPFLAGS!$CPPFLAGS$ac_delim ac_ct_CC!$ac_ct_CC$ac_delim -EXEEXT!$EXEEXT$ac_delim -OBJEXT!$OBJEXT$ac_delim CPP!$CPP$ac_delim GREP!$GREP$ac_delim EGREP!$EGREP$ac_delim HAVE_SELINUX!$HAVE_SELINUX$ac_delim -CXX!$CXX$ac_delim -CXXFLAGS!$CXXFLAGS$ac_delim -ac_ct_CXX!$ac_ct_CXX$ac_delim CXXCPP!$CXXCPP$ac_delim UPSTREAM_STP_LINK_FLAGS!$UPSTREAM_STP_LINK_FLAGS$ac_delim STP_NEEDS_BOOST!$STP_NEEDS_BOOST$ac_delim @@ -7474,7 +7566,7 @@ LIBOBJS!$LIBOBJS$ac_delim LTLIBOBJS!$LTLIBOBJS$ac_delim _ACEOF - if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 91; then + if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 92; then break elif $ac_last_try; then { { echo "$as_me:$LINENO: error: could not make $CONFIG_STATUS" >&5 diff --git a/lib/Core/Common.cpp b/lib/Core/Common.cpp index 575a1f1b..c58e121a 100644 --- a/lib/Core/Common.cpp +++ b/lib/Core/Common.cpp @@ -8,6 +8,8 @@ //===----------------------------------------------------------------------===// #include "Common.h" +#include "llvm/ADT/StringRef.h" +#include "llvm/Support/raw_ostream.h" #include <stdlib.h> #include <stdio.h> @@ -22,16 +24,72 @@ using namespace klee; FILE* klee::klee_warning_file = NULL; FILE* klee::klee_message_file = NULL; -static void klee_vfmessage(FILE *fp, const char *pfx, const char *msg, +static const char* warningPrefix = "WARNING"; +static const char* warningOncePrefix = "WARNING ONCE"; +static const char* errorPrefix = "ERROR"; +static const char* notePrefix = "NOTE"; + +static bool shouldSetColor(const char* pfx, const char* msg, const char* prefixToSearchFor) +{ + if (pfx && strcmp(pfx, prefixToSearchFor) == 0) + return true; + + if (llvm::StringRef(msg).startswith(prefixToSearchFor)) + return true; + + return false; +} + +static void klee_vfmessage(FILE *fp, const char *pfx, const char *msg, va_list ap) { if (!fp) return; - fprintf(fp, "KLEE: "); - if (pfx) fprintf(fp, "%s: ", pfx); + llvm::raw_fd_ostream fdos(fileno(fp), /*shouldClose=*/false, /*unbuffered=*/ true); + bool modifyConsoleColor = fdos.is_displayed() && (fp == stderr); + + if (modifyConsoleColor) { + + // Warnings + if (shouldSetColor(pfx, msg, warningPrefix)) + fdos.changeColor(llvm::raw_ostream::MAGENTA, + /*bold=*/ false, + /*bg=*/ false); + + // Once warning + if (shouldSetColor(pfx, msg, warningOncePrefix)) + fdos.changeColor(llvm::raw_ostream::MAGENTA, + /*bold=*/ true, + /*bg=*/ false); + + // Errors + if (shouldSetColor(pfx, msg, errorPrefix)) + fdos.changeColor(llvm::raw_ostream::RED, + /*bold=*/ true, + /*bg=*/ false); + + // Notes + if (shouldSetColor(pfx, msg, notePrefix)) + fdos.changeColor(llvm::raw_ostream::WHITE, + /*bold=*/ true, + /*bg=*/ false); + + } + + fdos << "KLEE: "; + if (pfx) fdos << pfx << ": "; + + // FIXME: Can't use fdos here because we need to print + // a variable number of arguments and do substitution vfprintf(fp, msg, ap); - fprintf(fp, "\n"); fflush(fp); + + fdos << "\n"; + + if (modifyConsoleColor) + fdos.resetColor(); + + fdos.flush(); } /* Prints a message/warning. @@ -73,7 +131,7 @@ void klee::klee_message_to_file(const char *msg, ...) { void klee::klee_error(const char *msg, ...) { va_list ap; va_start(ap, msg); - klee_vmessage("ERROR", false, msg, ap); + klee_vmessage(errorPrefix, false, msg, ap); va_end(ap); exit(1); } @@ -81,7 +139,7 @@ void klee::klee_error(const char *msg, ...) { void klee::klee_warning(const char *msg, ...) { va_list ap; va_start(ap, msg); - klee_vmessage("WARNING", false, msg, ap); + klee_vmessage(warningPrefix, false, msg, ap); va_end(ap); } @@ -104,7 +162,7 @@ void klee::klee_warning_once(const void *id, const char *msg, ...) { va_list ap; va_start(ap, msg); - klee_vmessage("WARNING ONCE", false, msg, ap); + klee_vmessage(warningOncePrefix, false, msg, ap); va_end(ap); } } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d2978642..314e5b82 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -78,12 +78,17 @@ #endif #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" -#include "llvm/Support/CallSite.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/Process.h" #include "llvm/Support/raw_ostream.h" +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) +#include "llvm/Support/CallSite.h" +#else +#include "llvm/IR/CallSite.h" +#endif + #include <cassert> #include <algorithm> #include <iomanip> @@ -139,10 +144,6 @@ namespace { cl::init(false)); cl::opt<bool> - UseAsmAddresses("use-asm-addresses", - cl::init(false)); - - cl::opt<bool> RandomizeFork("randomize-fork", cl::init(false), cl::desc("Randomly swap the true and false states on a fork (default=off)")); @@ -580,32 +581,9 @@ void Executor::initializeGlobals(ExecutionState &state) { } else { LLVM_TYPE_Q Type *ty = i->getType()->getElementType(); uint64_t size = kmodule->targetData->getTypeStoreSize(ty); - MemoryObject *mo = 0; - -#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) - if (UseAsmAddresses && i->getName()[0]=='\01') { -#else - if (UseAsmAddresses && !i->getName().empty()) { -#endif - char *end; -#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) - uint64_t address = ::strtoll(i->getName().str().c_str()+1, &end, 0); -#else - uint64_t address = ::strtoll(i->getName().str().c_str(), &end, 0); -#endif - - if (end && *end == '\0') { - klee_message("NOTE: allocated global at asm specified address: %#08llx" - " (%llu bytes)", - (long long) address, (unsigned long long) size); - mo = memory->allocateFixed(address, size, &*i); - mo->isUserSpecified = true; // XXX hack; - } - } - + MemoryObject *mo = memory->allocate(size, false, true, &*i); if (!mo) - mo = memory->allocate(size, false, true, &*i); - assert(mo && "out of memory"); + llvm::report_fatal_error("out of memory"); ObjectState *os = bindObjectInState(state, mo, false); globalObjects.insert(std::make_pair(i, mo)); globalAddresses.insert(std::make_pair(i, mo->getBaseExpr())); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 7d82332c..523b3648 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -20,7 +20,9 @@ #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Module/KModule.h" -#include "llvm/Support/CallSite.h" + +#include "llvm/ADT/Twine.h" + #include <vector> #include <string> #include <map> diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index f6b3dd5e..56f18e6b 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -38,9 +38,6 @@ #endif #endif -#include "llvm/Support/CallSite.h" - - #include <cassert> using namespace klee; diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 4c1e2b86..5f9f8dc6 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -32,14 +32,21 @@ #endif #include "llvm/ExecutionEngine/JIT.h" #include "llvm/ExecutionEngine/GenericValue.h" -#include "llvm/Support/CallSite.h" #include "llvm/Support/DynamicLibrary.h" #include "llvm/Support/raw_ostream.h" + #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0) #include "llvm/Target/TargetSelect.h" #else #include "llvm/Support/TargetSelect.h" #endif + +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) +#include "llvm/Support/CallSite.h" +#else +#include "llvm/IR/CallSite.h" +#endif + #include <setjmp.h> #include <signal.h> diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 2610f17e..e33d2a56 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -34,10 +34,14 @@ #include "llvm/Instructions.h" #include "llvm/Module.h" #endif -#include "llvm/Support/CallSite.h" -#include "llvm/Support/CFG.h" #include "llvm/Support/CommandLine.h" +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) +#include "llvm/Support/CallSite.h" +#else +#include "llvm/IR/CallSite.h" +#endif + #include <cassert> #include <fstream> #include <climits> diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index e664d1ae..0e564fe5 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -52,11 +52,18 @@ #include "llvm/Type.h" #endif #include "llvm/Support/CommandLine.h" -#include "llvm/Support/CFG.h" #include "llvm/Support/Process.h" #include "llvm/Support/Path.h" #include "llvm/Support/FileSystem.h" +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) +#include "llvm/Support/CallSite.h" +#include "llvm/Support/CFG.h" +#else +#include "llvm/IR/CallSite.h" +#include "llvm/IR/CFG.h" +#endif + #include <fstream> #include <unistd.h> @@ -190,8 +197,13 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, SmallString<128> current(objectFilename); if(sys::fs::make_absolute(current)) { bool exists = false; + +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) error_code ec = sys::fs::exists(current.str(), exists); if (ec == errc::success && exists) { +#else + if (!sys::fs::exists(current.str(), exists)) { +#endif objectFilename = current.c_str(); } } @@ -501,6 +513,15 @@ void StatsTracker::writeIStats() { for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); fnIt != fn_ie; ++fnIt) { if (!fnIt->isDeclaration()) { + // Always try to write the filename before the function name, as otherwise + // KCachegrind can create two entries for the function, one with an + // unnamed file and one without. + const InstructionInfo &ii = executor.kmodule->infos->getFunctionInfo(fnIt); + if (ii.file != sourceFile) { + of << "fl=" << ii.file << "\n"; + sourceFile = ii.file; + } + of << "fn=" << fnIt->getName().str() << "\n"; for (Function::iterator bbIt = fnIt->begin(), bb_ie = fnIt->end(); bbIt != bb_ie; ++bbIt) { diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp index e1076d43..7d9b7284 100644 --- a/lib/Module/Checks.cpp +++ b/lib/Module/Checks.cpp @@ -45,7 +45,6 @@ #include "llvm/Pass.h" #include "llvm/Transforms/Scalar.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" -#include "llvm/Support/CallSite.h" using namespace llvm; using namespace klee; diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp index 8d27e426..7e9a9e26 100644 --- a/lib/Module/InstructionInfoTable.cpp +++ b/lib/Module/InstructionInfoTable.cpp @@ -21,17 +21,28 @@ #include "llvm/IntrinsicInst.h" #include "llvm/Module.h" #endif -#include "llvm/Linker.h" + +# if LLVM_VERSION_CODE < LLVM_VERSION(3,5) #include "llvm/Assembly/AssemblyAnnotationWriter.h" -#include "llvm/Support/FormattedStream.h" -#include "llvm/Support/CFG.h" #include "llvm/Support/InstIterator.h" +#include "llvm/Linker.h" +#else +#include "llvm/IR/AssemblyAnnotationWriter.h" +#include "llvm/IR/InstIterator.h" +#include "llvm/Linker/Linker.h" +#endif + +#include "llvm/Support/FormattedStream.h" #include "llvm/Support/raw_ostream.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3,5) +#include "llvm/IR/DebugInfo.h" +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) #include "llvm/DebugInfo.h" #else #include "llvm/Analysis/DebugInfo.h" #endif + #include "llvm/Analysis/ValueTracking.h" #include "llvm/Support/ErrorHandling.h" @@ -110,22 +121,31 @@ InstructionInfoTable::InstructionInfoTable(Module *m) for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); fnIt != fn_ie; ++fnIt) { + // We want to ensure that as all instructions have source information, if + // available. Clang sometimes will not write out debug information on the + // initial instructions in a function (correspond to the formal parameters), + // so we first search forward to find the first instruction with debug info, + // if any. + const std::string *initialFile = &dummyString; + unsigned initialLine = 0; + for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt); it != ie; + ++it) { + if (getInstructionDebugInfo(&*it, initialFile, initialLine)) + break; + } + + const std::string *file = initialFile; + unsigned line = initialLine; for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt); it != ie; ++it) { - const std::string *initialFile = &dummyString; - unsigned initialLine = 0; Instruction *instr = &*it; - unsigned assemblyLine = 0; + unsigned assemblyLine = lineTable[instr]; + + // Update our source level debug information. + getInstructionDebugInfo(instr, file, line); - std::map<const Instruction*, unsigned>::const_iterator ltit = - lineTable.find(instr); - if (ltit!=lineTable.end()) - assemblyLine = ltit->second; - getInstructionDebugInfo(instr, initialFile, initialLine); infos.insert(std::make_pair(instr, - InstructionInfo(id++, - *initialFile, - initialLine, + InstructionInfo(id++, *file, line, assemblyLine))); } } diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 57e0c4fe..1334b58c 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -10,6 +10,7 @@ // FIXME: This does not belong here. #include "../Core/Common.h" +#define DEBUG_TYPE "KModule" #include "klee/Internal/Module/KModule.h" #include "Passes.h" @@ -42,8 +43,13 @@ #endif -#include "llvm/PassManager.h" +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) #include "llvm/Support/CallSite.h" +#else +#include "llvm/IR/CallSite.h" +#endif + +#include "llvm/PassManager.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Support/raw_os_ostream.h" @@ -51,7 +57,6 @@ #include "llvm/Transforms/Scalar.h" #include <llvm/Transforms/Utils/Cloning.h> -#include <llvm/Support/InstIterator.h> #include <sstream> @@ -224,56 +229,11 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType, } #endif -/// This function will take try to inline all calls to \p functionName -/// in the module \p module . -/// -/// It is intended that this function be used for inling calls to -/// check functions like <tt>klee_div_zero_check()</tt> -static void inlineChecks(Module *module, const char * functionName) { - std::vector<CallSite> checkCalls; - Function* runtimeCheckCall = module->getFunction(functionName); - if (runtimeCheckCall == 0) - { - KLEE_DEBUG(klee_warning("Failed to inline %s because no calls were made " - "to it in module", functionName)); - return; - } - - for (Value::use_iterator i = runtimeCheckCall->use_begin(), - e = runtimeCheckCall->use_end(); i != e; ++i) - if (isa<InvokeInst>(*i) || isa<CallInst>(*i)) { - CallSite cs(*i); - if (!cs.getCalledFunction()) - continue; - checkCalls.push_back(cs); - } - - unsigned int successCount=0; - unsigned int failCount=0; - InlineFunctionInfo IFI(0,0); - for ( std::vector<CallSite>::iterator ci = checkCalls.begin(), - cie = checkCalls.end(); - ci != cie; ++ci) - { - // Try to inline the function - if (InlineFunction(*ci,IFI)) - ++successCount; - else - { - ++failCount; - klee_warning("Failed to inline function %s", functionName); - } - } - - KLEE_DEBUG(klee_message("Tried to inline calls to %s. %u successes, " - "%u failures", functionName, successCount, - failCount)); -} void KModule::addInternalFunction(const char* functionName){ Function* internalFunction = module->getFunction(functionName); if (!internalFunction) { - KLEE_DEBUG_WITH_TYPE("KModule", klee_warning( + KLEE_DEBUG(klee_warning( "Failed to add internal function %s. Not found.", functionName)); return ; } diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index be1ea4c1..3811003e 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -41,15 +41,24 @@ #include "llvm/Module.h" #endif +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) #include "llvm/Linker.h" #include "llvm/Assembly/AssemblyAnnotationWriter.h" -#include "llvm/Support/CFG.h" -#include "llvm/Support/CallSite.h" -#include "llvm/Support/InstIterator.h" +#else +#include "llvm/Linker/Linker.h" +#include "llvm/IR/AssemblyAnnotationWriter.h" +#endif + #include "llvm/Support/raw_ostream.h" #include "llvm/Analysis/ValueTracking.h" #include "llvm/Support/Path.h" +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) +#include "llvm/Support/CallSite.h" +#else +#include "llvm/IR/CallSite.h" +#endif + #include <map> #include <set> #include <fstream> diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index ed1e0e34..ce43cd96 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -19,7 +19,6 @@ #include "llvm/PassManager.h" #include "llvm/Analysis/Passes.h" #include "llvm/Analysis/LoopPass.h" -#include "llvm/Analysis/Verifier.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/DynamicLibrary.h" @@ -35,19 +34,18 @@ #endif #endif +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#include "llvm/IR/Verifier.h" +#else +#include "llvm/Analysis/Verifier.h" +#endif + #include "llvm/Target/TargetMachine.h" #include "llvm/Transforms/IPO.h" #include "llvm/Transforms/Scalar.h" -#include "llvm/Support/PassNameParser.h" #include "llvm/Support/PluginLoader.h" using namespace llvm; -#if 0 -// Pass Name Options as generated by the PassNameParser -static cl::list<const PassInfo*, bool, PassNameParser> - OptimizationList(cl::desc("Optimizations available:")); -#endif - // Don't verify at the end static cl::opt<bool> DontVerify("disable-verify", cl::ReallyHidden); @@ -177,9 +175,12 @@ void Optimize(Module* M) { #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) // Add an appropriate TargetData instance for this module... addPass(Passes, new TargetData(M)); -#else +#elif LLVM_VERSION_CODE < LLVM_VERSION(3, 5) // Add an appropriate DataLayout instance for this module... addPass(Passes, new DataLayout(M)); +#else + // Add an appropriate DataLayout instance for this module... + addPass(Passes, new DataLayoutPass(M)); #endif // DWD - Run the opt standard pass list as well. diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index d5598d1d..5484a319 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -4,6 +4,10 @@ #include "klee/Internal/System/Time.h" #include "klee/Statistics.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#include "llvm/Support/FileSystem.h" +#endif + // // The KLEE Symbolic Virtual Machine // @@ -19,7 +23,11 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, const std::string& commentSign, int queryTimeToLog) : solver(_solver), +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), +#else os(path.c_str(), ErrorInfo), +#endif BufferString(""), logBuffer(BufferString), queryCount(0), diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp index 74ffe3ba..ef59b2a9 100644 --- a/lib/Support/TreeStream.cpp +++ b/lib/Support/TreeStream.cpp @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// +#define DEBUG_TYPE "TreeStreamWriter" #include "klee/Internal/ADT/TreeStream.h" #include "klee/Internal/Support/Debug.h" @@ -107,8 +108,7 @@ void TreeStreamWriter::readStream(TreeStreamID streamID, std::ifstream is(path.c_str(), std::ios::in | std::ios::binary); assert(is.good()); - KLEE_DEBUG_WITH_TYPE("TreeStreamWriter", - llvm::errs() << "finding chain for: " << streamID << "\n"); + KLEE_DEBUG(llvm::errs() << "finding chain for: " << streamID << "\n"); std::map<unsigned,unsigned> parents; std::vector<unsigned> roots; @@ -202,3 +202,4 @@ void TreeOStream::flush() { assert(writer); writer->flush(); } + diff --git a/test/CXX/StaticDestructor.cpp b/test/CXX/StaticDestructor.cpp index 6e6f033d..adc449a5 100644 --- a/test/CXX/StaticDestructor.cpp +++ b/test/CXX/StaticDestructor.cpp @@ -2,7 +2,7 @@ // RUN: %llvmgxx %s -emit-llvm -g -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --optimize=false --libc=uclibc --no-output %t1.bc 2> %t1.log +// RUN: %klee --output-dir=%t.klee-out --optimize=false --libc=klee --no-output %t1.bc 2> %t1.log // RUN: grep ":17: memory error" %t1.log #include <cassert> diff --git a/test/Coverage/ReadArgs.c b/test/Coverage/ReadArgs.c index 1001dac1..8eae53a1 100644 --- a/test/Coverage/ReadArgs.c +++ b/test/Coverage/ReadArgs.c @@ -1,7 +1,7 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: echo " --output-dir=%t.klee-out " > %t1.args -// RUN: %klee --read-args %t1.args %t1.bc +// RUN: %klee @%t1.args %t1.bc // RUN: test -d %t.klee-out int main() { diff --git a/test/Feature/AsmAddresses.c b/test/Feature/AsmAddresses.c deleted file mode 100644 index cfe566af..00000000 --- a/test/Feature/AsmAddresses.c +++ /dev/null @@ -1,25 +0,0 @@ -// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s -// RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --exit-on-error --use-asm-addresses %t.bc - -// RUN: %llvmgcc -emit-llvm -DOVERLAP -g -c -o %t.bc %s -// RUN: rm -rf %t.klee-out -// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --use-asm-addresses %t.bc - -#include <assert.h> - - -volatile unsigned char x0 __asm ("0x0021"); -volatile unsigned char whee __asm ("0x0WHEE"); - -#ifdef OVERLAP -volatile unsigned int y0 __asm ("0x0030"); -volatile unsigned int y1 __asm ("0x0032"); -#endif - -int main() { - assert(&x0 == (void*) 0x0021); - assert(&whee != (void*) 0x0); - - return 0; -} diff --git a/test/Feature/SourceMapping.c b/test/Feature/SourceMapping.c new file mode 100644 index 00000000..9835d701 --- /dev/null +++ b/test/Feature/SourceMapping.c @@ -0,0 +1,55 @@ +// Check that we properly associate instruction level statistics with source +// file and line. +// +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc +// RUN: FileCheck < %t.klee-out/run.istats %s + +// CHECK: positions: instr line +// CHECK: ob={{.*}}/SourceMapping.c{{.*}}/assembly.ll + +// Assuming the compiler doesn't reorder things, f0 should be first, and it +// should immediately follow the first file name marker. +// CHECK: fl={{.*}}/SourceMapping.c +// CHECK-NEXT: fn=f0 + +// Ensure we have a known position for the first instruction (instr and line +// should be non-zero). + +// CHECK-NEXT: {{[1-9][0-9]*}} {{[1-9][0-9]*}} + + +// Ensure we have the right line number (and check called function markers). +// CHECK: fn=f1 +// CHECK: cfn=f0 +// CHECK-NEXT: calls=1 {{[1-9][0-9]*}} +// CHECK-NEXT: {{[1-9][0-9]*}} 48 {{.*}} + +// This check just brackets the checks above, to make sure they fall in the +// appropriate region of the run.istats file. +// +// CHECK: fn=main + + + + + + + +// KEEP THIS AS LINE 40 + +int f0(int a, int b) { + return a + b; +} + +int f1(int a, int b) { + // f0 is called on line 48 + return f0(a, b); +} + +int main() { + int x = f1(1, 2); + + return x; +} diff --git a/test/Makefile b/test/Makefile index 31896075..02d0a36f 100644 --- a/test/Makefile +++ b/test/Makefile @@ -23,11 +23,10 @@ include Makefile.tests #===------------------------------------------------------------------------===# ULIMIT = ulimit -t 600 ; ulimit -d 512000 ; -# FIXME: Fix test suite so we can run lit in parallel. ifdef VERBOSE -LIT_ARGS := -j1 -v +LIT_ARGS := -v else -LIT_ARGS := -j1 -s -v +LIT_ARGS := -s -v endif ifdef TESTSUITE diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 4411f73a..a7f2fbc6 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -164,11 +164,6 @@ namespace { cl::desc("Directory to write results in (defaults to klee-out-N)"), cl::init("")); - // this is a fake entry, its automagically handled - cl::list<std::string> - ReadArgsFilesFake("read-args", - cl::desc("File to read arguments from (one arg per line)")); - cl::opt<bool> ReplayKeepSymbolic("replay-keep-symbolic", cl::desc("Replay the test cases only by asserting " @@ -619,48 +614,15 @@ static std::string strip(std::string &in) { return in.substr(lead, trail-lead); } -static void readArgumentsFromFile(char *file, std::vector<std::string> &results) { - std::ifstream f(file); - assert(f.is_open() && "unable to open input for reading arguments"); - while (!f.eof()) { - std::string line; - std::getline(f, line); - line = strip(line); - if (!line.empty()) - results.push_back(line); - } - f.close(); -} - static void parseArguments(int argc, char **argv) { - std::vector<std::string> arguments; - - for (int i=1; i<argc; i++) { - if (!strcmp(argv[i],"--read-args") && i+1<argc) { - readArgumentsFromFile(argv[++i], arguments); - } else { - arguments.push_back(argv[i]); - } - } - - int numArgs = arguments.size() + 1; - const char **argArray = new const char*[numArgs+1]; - argArray[0] = argv[0]; - argArray[numArgs] = 0; - for (int i=1; i<numArgs; i++) { - argArray[i] = arguments[i-1].c_str(); - } - #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) - cl::ParseCommandLineOptions(numArgs, (const char**) argArray, " klee\n"); + // This version always reads response files + cl::ParseCommandLineOptions(argc, (const char**) argv, " klee\n"); #else - cl::ParseCommandLineOptions(numArgs, (char**) argArray, " klee\n"); + cl::ParseCommandLineOptions(argc, (char**) argv, " klee\n", /*ReadResponseFiles=*/ true); #endif - delete[] argArray; } - - static int initEnv(Module *mainModule) { /* @@ -1529,7 +1491,18 @@ int main(int argc, char **argv, char **envp) { << handler->getNumPathsExplored() << "\n"; stats << "KLEE: done: generated tests = " << handler->getNumTestCases() << "\n"; + + bool useColors = llvm::errs().is_displayed(); + if (useColors) + llvm::errs().changeColor(llvm::raw_ostream::GREEN, + /*bold=*/true, + /*bg=*/false); + llvm::errs() << stats.str(); + + if (useColors) + llvm::errs().resetColor(); + handler->getInfoStream() << stats.str(); BufferPtr.take(); |