diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-02-11 06:01:56 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-02-14 23:55:24 +0000 |
commit | 7f9afabacfecadf2be0a7451049d2f96ef8f203b (patch) | |
tree | e59c06088dd2b5ef14f2b123a1c31cb10efe440f /.travis | |
parent | 5960bc6387df8ec89e3e98ae3867b0a3c025033b (diff) | |
download | klee-7f9afabacfecadf2be0a7451049d2f96ef8f203b.tar.gz |
Add TravisCI and Docker support for building KLEE with Z3 support
Diffstat (limited to '.travis')
-rwxr-xr-x | .travis/klee.sh | 28 | ||||
-rwxr-xr-x | .travis/solvers.sh | 27 |
2 files changed, 54 insertions, 1 deletions
diff --git a/.travis/klee.sh b/.travis/klee.sh index fbce61e7..0f855b46 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -1,6 +1,7 @@ #!/bin/bash -x # Make sure we exit if there is a failure set -e +: ${SOLVERS?"Solvers must be specified"} # Calculate LLVM branch name to retrieve missing files from SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')" @@ -43,6 +44,30 @@ COVERAGE_FLAGS="" if [ ${COVERAGE} -eq 1 ]; then COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage' fi + + +############################################################################### +# Handle setting up solver configure flags for KLEE +############################################################################### +KLEE_Z3_CONFIGURE_OPTION="" +KLEE_STP_CONFIGURE_OPTION="" +SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') + +for solver in ${SOLVER_LIST}; do + echo "Setting configuration option for ${solver}" + case ${solver} in + STP) + KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build" + ;; + Z3) + echo "Z3" + KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr" + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac +done ############################################################################### # KLEE ############################################################################### @@ -57,7 +82,8 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \ --with-llvmcc=${KLEE_CC} \ --with-llvmcxx=${KLEE_CXX} \ - --with-stp="${BUILD_DIR}/stp/build" \ + ${KLEE_STP_CONFIGURE_OPTION} \ + ${KLEE_Z3_CONFIGURE_OPTION} \ ${KLEE_UCLIBC_CONFIGURE_OPTION} \ CXXFLAGS="${COVERAGE_FLAGS}" \ && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ diff --git a/.travis/solvers.sh b/.travis/solvers.sh new file mode 100755 index 00000000..db717f2d --- /dev/null +++ b/.travis/solvers.sh @@ -0,0 +1,27 @@ +#!/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" + # Should we install libz3-dbg too? + sudo apt-get -y install libz3 libz3-dev + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac +done |