9 files changed, 0 insertions, 476 deletions
diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh
deleted file mode 100755
index bd34d843..00000000
--- a/.travis/install-llvm-and-runtime-compiler.sh
+++ /dev/null
@@ -1,27 +0,0 @@
-#!/bin/bash -x
-set -ev
-
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev
-
-  sudo apt-get install -y llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION}
-  sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_VERSION} 20
-  sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_VERSION} 20
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  # We use our own local cache if possible
-  set +e
-  brew install $HOME/Library/Caches/Homebrew/llvm\@${LLVM_VERSION}*.bottle.tar.gz
-  RES=$?
-  set -ev
-  if [ ${RES} -ne 0 ]; then
-    # This might build the llvm package use a time out to avoid dumping log information
-    brew install -v --build-bottle "llvm@${LLVM_VERSION}"
-    # Now bottle the brew
-    brew bottle llvm\@${LLVM_VERSION}
-    # Not make sure it's cached
-    cp llvm\@${LLVM_VERSION}*.bottle.tar.gz $HOME/Library/Caches/Homebrew/
-  fi
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh
deleted file mode 100755
index 0bc26616..00000000
--- a/.travis/install-tcmalloc.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/bash -x
-set -ev
-
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then
-    # Get tcmalloc release
-    wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz
-    tar xfz gperftools-2.4.tar.gz
-    cd gperftools-2.4
-    ./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc  --enable-minimal --prefix=/usr
-    make
-    sudo make install
-  fi
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then
-    echo "Error: Requested to install TCMalloc on macOS, which is not supported"
-    exit 1
-  fi
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
diff --git a/.travis/klee.sh b/.travis/klee.sh
deleted file mode 100755
index 5c5a15b5..00000000
--- a/.travis/klee.sh
+++ /dev/null
@@ -1,202 +0,0 @@
-#!/bin/bash -x
-# Make sure we exit if there is a failure
-set -e
-: ${SOLVERS?"Solvers must be specified"}
-
-coverage_setup()
-{
-  # Zero coverage for any file, e.g. previous tests
-  lcov --directory . --no-external --zerocounters
-  # Create a baseline by capturing any file used for compilation, no execution yet
-  lcov --rc lcov_branch_coverage=1 --directory . --base-directory=${KLEE_SRC} --no-external --capture --initial --output-file coverage_base.info
-  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info
-  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info
-}
-
-coverageup()
-{
-  # Create report
-  # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped)
-  lcov --rc lcov_branch_coverage=1 --directory . --base-directory=${KLEE_SRC} --no-external --capture --output-file coverage.info
-  # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests)
-  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info
-  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info
-  # Combine baseline and measured coverage
-  lcov --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info
-  # Debug info
-  lcov --rc lcov_branch_coverage=1 --list coverage_all.info
-  # Uploading report to CodeCov
-  bash <(curl -s https://codecov.io/bash) -R ${KLEE_SRC} -X gcov -y ${KLEE_SRC}/.codecov.yml -f coverage_all.info -F $1
-}
-
-###############################################################################
-# Select the compiler to use to generate LLVM bitcode
-###############################################################################
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  KLEE_CC=/usr/bin/clang-${LLVM_VERSION}
-  KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION}
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  KLEE_CC=/usr/local/bin/clang-${LLVM_VERSION}
-  KLEE_CXX=/usr/local/bin/clang++-${LLVM_VERSION}
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
-
-###############################################################################
-# klee-uclibc
-###############################################################################
-if [ "${KLEE_UCLIBC}" != "0" ]; then
-    git clone --depth 1 -b ${KLEE_UCLIBC} git://github.com/klee/klee-uclibc.git
-    cd klee-uclibc
-    ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION}
-    make
-    KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE"
-    cd ../
-else
-    KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE"
-fi
-
-COVERAGE_FLAGS=""
-if [ ${COVERAGE} -eq 1 ]; then
-    COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage'
-fi
-
-
-###############################################################################
-# Handle setting up solver configure flags for KLEE
-###############################################################################
-SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
-
-# Set CMake configure options
-KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF"
-KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF"
-KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF"
-for solver in ${SOLVER_LIST}; do
-  echo "Setting CMake configuration option for ${solver}"
-  case ${solver} in
-  STP)
-    KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build"
-    ;;
-  Z3)
-    echo "Z3"
-    KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE"
-    ;;
-  metaSMT)
-    echo "metaSMT"
-    if [ "X${METASMT_DEFAULT}" == "X" ]; then
-      METASMT_DEFAULT=STP
-    fi
-    KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}"
-    ;;
-  *)
-    echo "Unknown solver ${solver}"
-    exit 1
-  esac
-done
-
-###############################################################################
-# Handle additional configure flags
-###############################################################################
-TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE")
-
-###############################################################################
-# Handle Sanitizer flags
-###############################################################################
-source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-
-###############################################################################
-# Handling LLVM configuration
-###############################################################################
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  LLVM_CONFIG="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config"
-  LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION}/build"
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}"
-  LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)"
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
-
-###############################################################################
-# KLEE
-###############################################################################
-mkdir klee
-cd klee
-
-GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/"
-if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then
-  KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE"
-else
-  KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE"
-fi
-
-if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then
-  CMAKE_BUILD_TYPE="RelWithDebInfo"
-else
-  CMAKE_BUILD_TYPE="Debug"
-fi
-
-# TODO: We should support Ninja too
-# Configure KLEE
-CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
-CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
-cmake \
-  -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" \
-  -DLLVMCC="${KLEE_CC}" \
-  -DLLVMCXX="${KLEE_CXX}" \
-  ${KLEE_STP_CONFIGURE_OPTION} \
-  ${KLEE_Z3_CONFIGURE_OPTION} \
-  ${KLEE_METASMT_CONFIGURE_OPTION} \
-  ${KLEE_UCLIBC_CONFIGURE_OPTION} \
-  ${TCMALLOC_OPTION} \
-  -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \
-  -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \
-  ${KLEE_ASSERTS_OPTION} \
-  -DENABLE_UNIT_TESTS=TRUE \
-  -DENABLE_SYSTEM_TESTS=TRUE \
-  -DLIT_ARGS="-v" \
-  ${KLEE_SRC}
-make
-
-###############################################################################
-# Unit tests
-###############################################################################
-# Prepare coverage information if COVERAGE is set
-if [ ${COVERAGE} -eq 1 ]; then
-  coverage_setup
-fi
-make unittests
-
-# Generate and upload coverage if COVERAGE is set
-if [ ${COVERAGE} -eq 1 ]; then
-  coverageup "unittests"
-fi
-
-###############################################################################
-# lit tests
-###############################################################################
-if [ ${COVERAGE} -eq 1 ]; then
-  coverage_setup
-fi
-make systemtests
-
-# If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends
-if [ "X${SOLVERS}" == "XmetaSMT" ]; then
-  metasmt_default=`echo "${METASMT_DEFAULT,,}"` # klee_opts and kleaver_opts use lowercase
-  available_metasmt_backends="btor stp z3 yices2 cvc4"
-  for backend in $available_metasmt_backends; do
-    if [ "X${metasmt_default}" != "X$backend" ]; then
-      if [ "$backend" == "cvc4" ]; then
-        for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done &
-      fi
-      lit -v --param klee_opts=-metasmt-backend=$backend --param kleaver_opts=-metasmt-backend=$backend test/
-    fi
-  done
-fi
-
-# Generate and upload coverage if COVERAGE is set
-if [ ${COVERAGE} -eq 1 ]; then
-  coverageup "systemtests"
-fi
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
deleted file mode 100755
index 5d5b669e..00000000
--- a/.travis/metaSMT.sh
+++ /dev/null
@@ -1,49 +0,0 @@
-#!/bin/bash -x
-
-set -e
-
-: ${METASMT_VERSION?"METASMT_VERSION not specified"}
-
-# Get Z3, libgmp, gperf (required by yices2)
-sudo apt-get -y install libz3 libz3-dev libgmp-dev gperf
-
-# Get Boost
-if [ "X${METASMT_BOOST_VERSION}" != "X" ]; then
-  # Taken from boost/hana/.travis.yml
-  BOOST_URL="http://sourceforge.net/projects/boost/files/boost/${METASMT_BOOST_VERSION}/boost_${METASMT_BOOST_VERSION//\./_}.tar.gz"
-  BOOST_DIR=`pwd`/boost-${METASMT_BOOST_VERSION}
-  mkdir -p ${BOOST_DIR}
-  wget --quiet -O - ${BOOST_URL} | tar --strip-components=1 -xz -C ${BOOST_DIR}
-  sudo ln -s ${BOOST_DIR}/boost /usr/include/boost
-else
-  sudo apt-get -y install libboost1.55-dev
-fi
-
-# Get CVC4
-wget http://www.informatik.uni-bremen.de/agra/systemc-verification/media/snapshots/cvc4-594301e.tar.gz
-tar -xf cvc4-594301e.tar.gz
-sudo mv cvc4 /usr
-
-# Clone
-git clone -b ${METASMT_VERSION} --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git
-cd metaSMT
-git submodule update --init
-
-source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
-  echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented"
-  exit 1
-fi
-
-# Bootstrap
-export BOOST_ROOT=/usr
-sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack
-./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 -DZ3_DIR=/usr -DCVC4_DIR=/usr/cvc4
-sudo cp deps/boolector-2.2.0/lib/* /usr/lib/              #
-sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ #
-sudo cp deps/minisat-git/lib/* /usr/lib/                  # hack
-sudo cp -r deps/stp-git-basic/lib/lib* /usr/lib/          #
-sudo cp deps/yices-2.5.1/lib/* /usr/lib/                  #
-
-# Build
-make -C build install
diff --git a/.travis/sanitizer_flags.sh b/.travis/sanitizer_flags.sh
deleted file mode 100644
index 4d3dce2c..00000000
--- a/.travis/sanitizer_flags.sh
+++ /dev/null
@@ -1,39 +0,0 @@
-# This file is meant to be included by shell scripts
-# that need to do a sanitized build.
-
-# Users of this script can use this variable
-# to detect if a Sanitized build was enabled.
-IS_SANITIZED_BUILD=0
-
-# AddressSanitizer
-if [ "X${ASAN_BUILD}" == "X1" ]; then
-  echo "Using ASan"
-  ASAN_CXX_FLAGS="-fsanitize=address -fno-omit-frame-pointer"
-  ASAN_C_FLAGS="${ASAN_CXX_FLAGS}"
-  ASAN_LD_FLAGS="${ASAN_CXX_FLAGS}"
-  IS_SANITIZED_BUILD=1
-else
-  echo "Not using ASan"
-  ASAN_CXX_FLAGS=""
-  ASAN_C_FLAGS=""
-  ASAN_LD_FLAGS=""
-fi
-
-# Undefined Behaviour Sanitizer
-if [ "X${UBSAN_BUILD}" == "X1" ]; then
-  echo "Using UBSan"
-  UBSAN_CXX_FLAGS="-fsanitize=undefined"
-  UBSAN_C_FLAGS="${UBSAN_CXX_FLAGS}"
-  UBSAN_LD_FLAGS="${UBSAN_CXX_FLAGS}"
-  IS_SANITIZED_BUILD=1
-else
-  echo "Not using UBSan"
-  UBSAN_CXX_FLAGS=""
-  UBSAN_C_FLAGS=""
-  UBSAN_LD_FLAGS=""
-fi
-
-# Set variables to be used by clients.
-SANITIZER_CXX_FLAGS="${ASAN_CXX_FLAGS} ${UBSAN_CXX_FLAGS}"
-SANITIZER_C_FLAGS="${ASAN_C_FLAGS} ${UBSAN_C_FLAGS}"
-SANITIZER_LD_FLAGS="${ASAN_LD_FLAGS} ${UBSAN_LD_FLAGS}"
diff --git a/.travis/solvers.sh b/.travis/solvers.sh
deleted file mode 100755
index b419d679..00000000
--- a/.travis/solvers.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/bin/bash -x
-# Make sure we exit if there is a failure
-set -e
-: ${SOLVERS?"Solvers must be specified"}
-
-SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
-
-for solver in ${SOLVER_LIST}; do
-  echo "Getting solver ${solver}"
-  case ${solver} in
-  STP)
-    echo "STP"
-    mkdir stp
-    cd stp
-    ${KLEE_SRC}/.travis/stp.sh
-    cd ../
-    ;;
-  Z3)
-    echo "Z3"
-    ${KLEE_SRC}/.travis/z3.sh
-    ;;
-  metaSMT)
-    echo "metaSMT"
-    ${KLEE_SRC}/.travis/metaSMT.sh
-    ;;
-  *)
-    echo "Unknown solver ${solver}"
-    exit 1
-  esac
-done
diff --git a/.travis/stp.sh b/.travis/stp.sh
deleted file mode 100755
index e8647839..00000000
--- a/.travis/stp.sh
+++ /dev/null
@@ -1,72 +0,0 @@
-#!/bin/bash -x
-
-# TODO: For OSX we can prepare bottled formulas for STP and minisat
-
-# Make sure we exit if there is a failure
-set -e
-
-STP_LOG="$(pwd)/stp-build.log"
-
-if [ "x${STP_VERSION}" != "x" ]; then
-  # Get Sanitizer flags
-  source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-
-  # Build minisat
-  git clone https://github.com/stp/minisat
-  cd minisat
-  mkdir build
-  cd build
-  MINISAT_DIR=`pwd`
-  if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-    CFLAGS="${SANITIZER_C_FLAGS}" \
-    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
-    cmake -DCMAKE_INSTALL_PREFIX=/usr ..
-  elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-    CFLAGS="${SANITIZER_C_FLAGS}" \
-    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
-    cmake -DCMAKE_INSTALL_PREFIX=/usr/local ..
-  else
-    echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-    exit 1
-  fi
-  make
-  sudo make install
-  cd ../../
-
-  # Determine STP build flags
-  if [ "X${STP_VERSION}" = "Xmaster" ]; then
-    # 5e9ca6339a2b3b000aa7a90c18601fdcf1212fe1 Silently BUILD_SHARED_LIBS removed. STATICCOMPILE does something similar
-    STP_CMAKE_FLAGS=( \
-      "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \
-      "-DSTATICCOMPILE:BOOL=ON" \
-    )
-  else
-    STP_CMAKE_FLAGS=( \
-      "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \
-      "-DBUILD_SHARED_LIBS:BOOL=OFF" \
-    )
-  fi
-
-  # Build STP
-  git clone --depth 1 -b "${STP_VERSION}" git://github.com/stp/stp.git src
-  mkdir build
-  cd build
-  # Disabling building of shared libs is a workaround.
-  # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8
-  CFLAGS="${SANITIZER_C_FLAGS}" \
-  CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
-  cmake "${STP_CMAKE_FLAGS[@]}" ../src
-
-  set +e # Do not exit if build fails because we need to display the log
-  make >> "${STP_LOG}" 2>&1
-else
-  echo "No STP_VERSION given or empty"
-  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}"
-  exit 1
-fi
diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh
deleted file mode 100755
index eefccdd2..00000000
--- a/.travis/testing-utils.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/bash -x
-# Make sure we exit if there is a failure
-set -e
-
-# The New CMake build system just needs the GTest sources regardless
-# of LLVM version.
-wget https://github.com/google/googletest/archive/release-1.7.0.zip
-unzip release-1.7.0.zip
-exit 0
diff --git a/.travis/z3.sh b/.travis/z3.sh
deleted file mode 100755
index 315d028c..00000000
--- a/.travis/z3.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/bash -x
-
-# Make sure we exit if there is a failure
-set -e
-
-source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
-  echo "Error: Requested Sanitized build but Z3 being used is not sanitized"
-  exit 1
-fi
-
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  # Should we install libz3-dbg too?
-  sudo apt-get -y install libz3 libz3-dev
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  set +e
-  brew install python@2
-  if [[ "X$?" != "X0" ]]; then
-     brew link --overwrite python@2
-  fi
-  set -e
-  brew install z3
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi