Skip to content

Use sanitizers in travis #968

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
96 changes: 36 additions & 60 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -1,52 +1,58 @@
language: cpp

cache: ccache

matrix:
include:

# Alpine Linux with musl-libc using g++
- os: linux
sudo: required
compiler: gcc
cache: ccache
services:
- docker
before_install:
- docker pull diffblue/cbmc-builder:alpine-0.0.1
- env > .env
install:
- docker run --env-file .env -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.1 sh -c "./travis_install.sh"
script:
- docker run --env-file .env -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.1 sh -c "./travis_script.sh"
env:
- PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.1"
- COMPILER="ccache g++"

# OS X using g++
- os: osx
sudo: false
compiler: gcc
cache: ccache
before_install:
#we create symlink to non-ccache gcc, to be used in tests
- mkdir bin ; ln -s /usr/bin/gcc bin/gcc
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
- export PATH=/usr/local/opt/ccache/libexec:$PATH
- ccache -M 1G
env: COMPILER=g++
env:
- COMPILER="g++"
- SAN_FLAGS="-fsanitize=address -fno-omit-frame-pointer"
- LINKFLAGS="${SAN_FLAGS}"

# OS X using clang++
- os: osx
sudo: false
compiler: clang
cache: ccache
before_install:
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
- export PATH=/usr/local/opt/ccache/libexec:$PATH
- ccache -M 1G
env:
- COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
- CCACHE_CPP2=yes
- CCACHE_CPP2="yes"
- SAN_FLAGS="-fsanitize=address -fno-omit-frame-pointer"
- LINKFLAGS="${SAN_FLAGS}"

# Ubuntu Linux with glibc using g++-5
- os: linux
sudo: false
compiler: gcc
cache: ccache
addons:
apt:
sources:
Expand All @@ -55,16 +61,18 @@ matrix:
- libwww-perl
- g++-5
- libubsan0
- libasan0
before_install:
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
env: COMPILER="g++-5"
env:
- COMPILER="g++-5"
- SAN_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer"
- LINKFLAGS="-fuse-ld=gold ${SAN_FLAGS}"

# Ubuntu Linux with glibc using g++-5, debug mode
- os: linux
sudo: false
compiler: gcc
cache: ccache
addons:
apt:
sources:
Expand All @@ -73,61 +81,39 @@ matrix:
- libwww-perl
- g++-5
- libubsan0
- libasan0
before_install:
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
env:
- COMPILER="g++-5"
- EXTRA_CXXFLAGS="-DDEBUG"
script: echo "Not running any tests for a debug build."

# Ubuntu Linux with glibc using clang++-3.7
- os: linux
sudo: false
compiler: clang
cache: ccache
addons:
apt:
sources:
- ubuntu-toolchain-r-test
- llvm-toolchain-precise-3.7
packages:
- libwww-perl
- clang-3.7
- libstdc++-5-dev
- libubsan0
before_install:
- mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
- export CCACHE_CPP2=yes
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
env:
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
- CCACHE_CPP2=yes
- COMPILER="g++-5"
- SAN_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer"
- LINKFLAGS="-fuse-ld=gold ${SAN_FLAGS}"
script:
- echo "Not running any tests for a debug build."

# Ubuntu Linux with glibc using clang++-3.7, debug mode
# Ubuntu Linux with glibc using clang++-3.8
- os: linux
sudo: false
compiler: clang
cache: ccache
addons:
apt:
sources:
- ubuntu-toolchain-r-test
- llvm-toolchain-precise-3.7
- llvm-toolchain-precise-3.8
packages:
- libwww-perl
- clang-3.7
- clang-3.8
- libstdc++-5-dev
- libubsan0
- libasan0
before_install:
- mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
- export CCACHE_CPP2=yes
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
- mkdir bin ; ln -s /usr/bin/clang-3.8 bin/gcc
env:
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
- CCACHE_CPP2=yes
- EXTRA_CXXFLAGS="-DDEBUG"
script: echo "Not running any tests for a debug build."
- COMPILER="ccache clang++-3.8 -Qunused-arguments -fcolor-diagnostics"
- CCACHE_CPP2="yes"
- SAN_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer"
- LINKFLAGS="-fuse-ld=gold ${SAN_FLAGS}"

- env: NAME="CPP-LINT"
install:
Expand All @@ -141,20 +127,10 @@ matrix:
before_cache:

install:
- COMMAND="make -C src minisat2-download" &&
eval ${PRE_COMMAND} ${COMMAND}
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
eval ${PRE_COMMAND} ${COMMAND}
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&
eval ${PRE_COMMAND} ${COMMAND}
- sh travis_install.sh

script:
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
eval ${PRE_COMMAND} ${COMMAND}
- COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
eval ${PRE_COMMAND} ${COMMAND}
- COMMAND="make -C unit test" && eval ${PRE_COMMAND} ${COMMAND}
- sh travis_script.sh

before_cache:
- ccache -s
16 changes: 16 additions & 0 deletions src/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,22 @@ symex.dir: languages goto-programs.dir pointer-analysis.dir \
goto-symex.dir linking.dir analyses.dir solvers.dir \
path-symex.dir goto-instrument.dir

clobber.dir: \
cpp.dir \
goto-programs.dir \
analyses.dir \
langapi.dir \
xmllang.dir \
assembler.dir \
solvers.dir \
java_bytecode.dir \
# Empty

memory-models.dir: \
ansi-c.dir \
linking.dir \
# Empty

# building for a particular directory

$(patsubst %, %.dir, $(DIRS)):
Expand Down
4 changes: 4 additions & 0 deletions travis_install.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
#!/bin/sh
set -e
make -C src minisat2-download
make -C src 'CXX=${COMPILER}' 'CXXFLAGS=${SAN_FLAGS} -O2 -g ${EXTRA_CXXFLAGS}' -j2 all clobber.dir memory-models.dir musketeer.dir
5 changes: 5 additions & 0 deletions travis_script.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
#!/bin/sh
set -e
make -C unit 'CXX=${COMPILER}' 'CXXFLAGS=${SAN_FLAGS} -O2 -g ${EXTRA_CXXFLAGS}' -j2
make -C unit test
if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ; env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test