diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-05-18 17:15:24 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-07-04 22:14:58 +0100 |
| commit | eb75a38011726d4a045f3db3edbfef924f62c737 (patch) | |
| tree | 52061a0fea581586bd8d6db90bbf70a024560d57 /scripts/build/solver-stp.sh | |
| parent | 6a8081d721a1fa6eba8e7efcbd1f3cf1ca4feb10 (diff) | |
| download | klee-eb75a38011726d4a045f3db3edbfef924f62c737.tar.gz | |
Extensive updates to the build script for dependencies and docker
Building/managing dependencies of KLEE are not easy. This script should change
this.
Features:
* script install different versions in their specific directories
This allows:
- to have different versions in parallel installed: llvm, solvers
- to have different optimization levels installed (Debug, no-debug,
assertions, optimized)
- to have different versions of instrumentation enabled (address, memory,
leakage, undefined behavior)
* the script is kept distribution agnostic: assuming basic packages are
installed (a compiler), use `scripts/build/ubuntu-dependencies.sh` to install
ubuntu specific ones
* the script does not install any file into system directories (sudo is not
required) files are only installed into a user specified BASE directory
The same scripts are used for either local setup (`scripts/build/local_install.sh`)
or create a docker image based of your current source folder (`scripts/build/build_docker.sh`)
Change the defaults permanently by modifying (`scripts/build/common-defaults.sh`)
or change them on the fly by providing them as environment variables on the
command line.
The same scripts are also used for TravisCI, so we test what we are using.
Diffstat (limited to 'scripts/build/solver-stp.sh')
| -rwxr-xr-x | scripts/build/solver-stp.sh | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/scripts/build/solver-stp.sh b/scripts/build/solver-stp.sh new file mode 100755 index 00000000..2e65ca30 --- /dev/null +++ b/scripts/build/solver-stp.sh @@ -0,0 +1,57 @@ +#!/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 +DIR="$(cd "$(dirname "$0")" && pwd)" +source "${DIR}/common-defaults.sh" + +cd ${BASE} +if [ "x${STP_VERSION}" != "x" ]; then + # Build minisat + git_clone_or_update https://github.com/stp/minisat "${BASE}/minisat" + mkdir -p "${BASE}/minisat/build" + cd "${BASE}/minisat/build" + MINISAT_DIR="$(pwd)" + if [[ "$TRAVIS_OS_NAME" == "linux" || "$TRAVIS_OS_NAME" == "osx" ]]; then + CFLAGS="${SANITIZER_C_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ + LDFLAGS="${SANITIZER_LD_FLAGS}" \ + cmake -DCMAKE_INSTALL_PREFIX="${BASE}/minisat-install" \ + ${SANITIZER_CMAKE_C_COMPILER} \ + ${SANITIZER_CMAKE_CXX_COMPILER} \ + "${BASE}/minisat" + else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 + fi + make + make install + + # Build STP + git_clone_or_update git://github.com/stp/stp.git "${BASE}/stp-${STP_VERSION}" ${STP_VERSION} + mkdir -p "${BASE}/stp-${STP_VERSION}-build" + cd "${BASE}/stp-${STP_VERSION}-build" + + STP_CMAKE_FLAGS=( \ + "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \ + -DNO_BOOST:BOOL=ON \ + -DENABLE_PYTHON_INTERFACE:BOOL=OFF \ + ${SANITIZER_CMAKE_C_COMPILER} \ + ${SANITIZER_CMAKE_CXX_COMPILER} \ + ) + # 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}" \ + LDFLAGS="${SANITIZER_LD_FLAGS}" \ + cmake ${STP_CMAKE_FLAGS} \ + -DCMAKE_PREFIX_PATH="${BASE}/minisat-install" "${BASE}/stp-${STP_VERSION}" \ + -DCMAKE_INSTALL_PREFIX="${BASE}/stp-${STP_VERSION}-install" + make + make install +else + echo "No STP_VERSION given or empty" + exit 1 +fi |
