1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
sudo: required
dist: trusty
language: cpp
compiler:
# FIXME: For now, building with Clang is disabled because the STP built with
# it hits an assertion failure during some tests. We should sort this out
# eventually and file the bug against STP or Clang whichever is appropriate,
# but for now it is easier to just reduce the number of configs we test
# anyway.
# - clang
- gcc
env:
###########################################################################
# Configurations
#
# Each line in the "env" section represents a set of environment variables
# passed to a build. Thus each line represents a different build
# configuration.
###########################################################################
# Check the matrix of:
# LLVM : {2.9, 3.4}
# SOLVERS : {Z3, STP, STP:Z3, metaSMT}
# STP_VERSION : {2.1.0, master}
# METASMT_DEFAULT : {btor, stp, z3}
# UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
# with Asserts enabled.
# COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set
matrix:
# Check KLEE CMake build
- LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
- LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
- LLVM_VERSION=2.9 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
# Test experimental metaSMT support
- LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=stp KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=stp KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=z3 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
- LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
# FIXME: Enable when we want to test LLVM3.5
#- LLVM_VERSION=3.5 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1
#- LLVM_VERSION=3.5 STP_VERSION=master KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
- LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
# Check at least one build with Asserts disabled.
- LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0
# Check at least one Debug+Asserts build
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0
# Check with TCMALLOC
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
- LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
global:
- secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
- secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
- secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg=
addons:
apt:
sources:
- sourceline: 'ppa:ubuntu-toolchain-r/test'
- sourceline: 'ppa:h-rayflood/llvm'
- sourceline: 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /'
key_url: 'http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key'
packages:
- gcc-4.8
- g++-4.8
- libcap-dev
- libselinux1-dev
- cmake
cache: apt
before_install:
###########################################################################
# Set up the locations to get various packages from
# We assume the Travis image uses Ubuntu 14.04 LTS
###########################################################################
# Update package information
- sudo apt-get update
###########################################################################
# Set up out of source build directory
###########################################################################
- export KLEE_SRC=`pwd`
- cd ../
- mkdir build
- cd build/
- export BUILD_DIR=`pwd`
###########################################################################
# Install stuff
###########################################################################
# Install LLVM and the LLVM bitcode compiler we require to build KLEE
- ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh
- ${KLEE_SRC}/.travis/install-tcmalloc.sh
# Install lit (llvm-lit is not available)
- sudo pip install lit
# Get SMT solvers
- ${KLEE_SRC}/.travis/solvers.sh
# Get needed utlities/libraries for testing KLEE
- mkdir test-utils/
- cd test-utils/
- ${KLEE_SRC}/.travis/testing-utils.sh
- cd ../
script:
# Build KLEE and run tests
- ${KLEE_SRC}/.travis/klee.sh
|
