about summary refs log tree commit diff homepage
path: root/.travis
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-02-11 06:01:56 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2016-02-14 23:55:24 +0000
commit7f9afabacfecadf2be0a7451049d2f96ef8f203b (patch)
treee59c06088dd2b5ef14f2b123a1c31cb10efe440f /.travis
parent5960bc6387df8ec89e3e98ae3867b0a3c025033b (diff)
downloadklee-7f9afabacfecadf2be0a7451049d2f96ef8f203b.tar.gz
Add TravisCI and Docker support for building KLEE with Z3 support
Diffstat (limited to '.travis')
-rwxr-xr-x.travis/klee.sh28
-rwxr-xr-x.travis/solvers.sh27
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