From 7f9afabacfecadf2be0a7451049d2f96ef8f203b Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 11 Feb 2016 06:01:56 +0000
Subject: Add TravisCI and Docker support for building KLEE with Z3 support

---
 .travis/klee.sh    | 28 +++++++++++++++++++++++++++-
 .travis/solvers.sh | 27 +++++++++++++++++++++++++++
 2 files changed, 54 insertions(+), 1 deletion(-)
 create mode 100755 .travis/solvers.sh

(limited to '.travis')

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
-- 
cgit 1.4.1