diff options
| -rw-r--r-- | .travis.yml | 7 | ||||
| -rwxr-xr-x | .travis/klee.sh | 6 | ||||
| -rwxr-xr-x | .travis/metaSMT.sh | 20 | ||||
| -rwxr-xr-x | .travis/solvers.sh | 4 | ||||
| -rw-r--r-- | MetaSMT.mk | 1 |
5 files changed, 37 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml index 158f8f76..45e93d22 100644 --- a/.travis.yml +++ b/.travis.yml @@ -19,7 +19,7 @@ env: # Check the matrix of: # LLVM : {2.9, 3.4} - # SOLVERS : {Z3, STP, STP:Z3} + # SOLVERS : {Z3, STP, STP:Z3, metaSMT} # STP_VERSION : {2.1.0, master} # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # with Asserts enabled. @@ -27,6 +27,9 @@ env: # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set matrix: + # Test experimental metaSMT support + - LLVM_VERSION=3.4 SOLVERS=metaSMT KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=metaSMT KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Test experimental Z3 support - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - LLVM_VERSION=2.9 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 @@ -65,6 +68,8 @@ before_install: # Set up the locations to get various packages from # We assume the Travis image uses Ubuntu 12.04 LTS ########################################################################### + # Needed for Boost + - sudo add-apt-repository -y ppa:boost-latest # Needed for CMake - sudo add-apt-repository -y ppa:kalakris/cmake # Needed for LLVM diff --git a/.travis/klee.sh b/.travis/klee.sh index 296e1c83..64087b11 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -51,6 +51,7 @@ fi ############################################################################### KLEE_Z3_CONFIGURE_OPTION="" KLEE_STP_CONFIGURE_OPTION="" +KLEE_METASMT_CONFIGURE_OPTION="" SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') for solver in ${SOLVER_LIST}; do @@ -63,6 +64,10 @@ for solver in ${SOLVER_LIST}; do echo "Z3" KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr" ;; + metaSMT) + echo "metaSMT" + KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root" + ;; *) echo "Unknown solver ${solver}" exit 1 @@ -87,6 +92,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ --with-llvmcxx=${KLEE_CXX} \ ${KLEE_STP_CONFIGURE_OPTION} \ ${KLEE_Z3_CONFIGURE_OPTION} \ + ${KLEE_METASMT_CONFIGURE_OPTION} \ ${KLEE_UCLIBC_CONFIGURE_OPTION} \ ${TCMALLOC_OPTION} \ CXXFLAGS="${COVERAGE_FLAGS}" \ diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh new file mode 100755 index 00000000..7a0d1eef --- /dev/null +++ b/.travis/metaSMT.sh @@ -0,0 +1,20 @@ +#!/bin/bash -x + +# Get Boost, Z3, libgmp +sudo apt-get -y install libboost1.55-dev libz3 libz3-dev libgmp-dev + +# Clone +git clone git://github.com/hoangmle/metaSMT.git +cd metaSMT +git clone git://github.com/agra-uni-bremen/dependencies.git + +# 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-1.5.118 --build minisat-git -DZ3_DIR=/usr +sudo cp deps/boolector-1.5.118/lib/* /usr/lib/ # +sudo cp deps/minisat-git/lib/* /usr/lib/ # hack +sudo cp deps/stp-git-basic/lib/* /usr/lib/ # + +# Build +make -C build install diff --git a/.travis/solvers.sh b/.travis/solvers.sh index db717f2d..d64c1077 100755 --- a/.travis/solvers.sh +++ b/.travis/solvers.sh @@ -20,6 +20,10 @@ for solver in ${SOLVER_LIST}; do # Should we install libz3-dbg too? sudo apt-get -y install libz3 libz3-dev ;; + metaSMT) + echo "metaSMT" + ${KLEE_SRC}/.travis/metaSMT.sh + ;; *) echo "Unknown solver ${solver}" exit 1 diff --git a/MetaSMT.mk b/MetaSMT.mk index 80f28a9b..dd34e5fd 100644 --- a/MetaSMT.mk +++ b/MetaSMT.mk @@ -7,5 +7,6 @@ ifeq ($(ENABLE_METASMT),1) CXX.Flags += $(metaSMT_CXXFLAGS) CXX.Flags += $(metaSMT_INCLUDES) CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) LIBS += $(metaSMT_LDLIBS) endif |