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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
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 a subset of the matrix of:
# LLVM : {3.4, 3.5, 3.6}
# SOLVERS : {Z3, STP, STP:Z3, metaSMT}
# STP_VERSION : {2.1.2, master}
# METASMT_VERSION : {v4.rc1}
# METASMT_DEFAULT : {BTOR, CVC4, STP, YICES2, Z3}
# METASMT_BOOST_VERSION : {x.y.z} // e.g. 1.60.0, libboost-dev will be used if unspecified
# UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
# DISABLE_ASSERTIONS: {0, 1}
# ENABLE_OPTIMIZED: {0, 1}
# COVERAGE: {0, 1}
# USE_TCMALLOC: {0, 1}
# COVERAGE when set indicates that coverage data should be uploaded to the service, only ONE job should have COVERAGE set
matrix:
# TODO: Add Doxygen build
# Check newer LLVMs
- LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
- LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
- LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
- LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
- LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
# ASan build. Do unoptimized build otherwise the optimizer might remove problematic code
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 ASAN_BUILD=1
# Test just using Z3
- LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
# Test we can build against STP master
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
# Check we can build latest klee-uclibc branch
- LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
# Test metaSMT support
- LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR 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=3.4 SOLVERS=STP STP_VERSION=2.1.2 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=2.1.2 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.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
# Coverage build
- LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0
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=
matrix:
include:
- os: osx
osx_image: xcode8.3
env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0
addons:
apt:
sources:
- sourceline: 'ppa:ubuntu-toolchain-r/test'
- sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.4 main'
key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
- sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.5 main'
key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
- sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.6 main'
key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
- sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.7 main'
key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
- 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
- libboost-program-options-dev
- libcap-dev
- libedit-dev
- libselinux1-dev
- cmake
- lcov
cache:
ccache: true
apt: true
directories:
- $HOME/Library/Caches/Homebrew
before_install:
###########################################################################
# Set up the locations to get various packages from
# We assume the Travis image uses Ubuntu 14.04 LTS
###########################################################################
# Update package information
- if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then sudo apt-get update; fi
- if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update && brew tap klee/klee && brew install ccache && export PATH="/usr/local/opt/ccache/libexec:$PATH" ; fi
###########################################################################
# 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 pip2 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
|
