Skip to content

TEST: DON'T REVIEW OR MERGE #2284

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 1 commit into from
Closed
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
285 changes: 4 additions & 281 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -1,288 +1,10 @@
language: cpp

jobs:
include:

- &formatting-stage
stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
env: NAME="clang-format"
addons:
apt:
packages:
- clang-format-3.8
install:
script: |
# Apparently update-alternatives doesn't work in Travis containers
mkdir -p priority-symlinks
ln -s /usr/bin/clang-format-3.8 priority-symlinks/clang-format
export PATH=${PWD}/priority-symlinks:${PATH}

# Now we can do the formatting pass
clang-format --version
git-clang-format-3.8 "${TRAVIS_BRANCH}"
git diff > formatted.diff
if [[ -s formatted.diff ]] ; then
echo 'Formatting error! The following diff shows the required changes'
echo 'Use the raw log to get a version of the diff that preserves spacing'
cat formatted.diff
exit 1
fi
echo 'No formatting errors found'
exit 0
before_cache:

- &linter-stage
stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
env: NAME="CPP-LINT"
install:
script: scripts/travis_lint.sh
before_cache:

- &string-table-check
stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
env: NAME="string-table"
install:
script: scripts/string_table_check.sh
before_cache:

- stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
env: NAME="DOXYGEN-CHECK"
addons:
apt:
sources:
- sourceline: 'deb http://packages.cloud.google.com/apt cloud-sdk-trusty main'
key_url: 'https://packages.cloud.google.com/apt/doc/apt-key.gpg'
packages:
- doxygen
- google-cloud-sdk
install:
script: scripts/travis_doxygen.sh
before_cache:
after_success:
# Google Cloud Integration
- export BRANCH="${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}"
- openssl aes-256-cbc -k ${GCLOUD_TRAVIS_CBMC_KEY}
-in gcloud-travis-cbmc.json.enc -out gcloud-travis-cbmc.json -d
- export G_KEY=${PWD}/gcloud-travis-cbmc.json
- gcloud auth activate-service-account --key-file ${G_KEY}

- scripts/publish_doc.sh

# Ubuntu Linux with glibc using g++-5
- stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
os: linux
sudo: false
compiler: gcc
cache: ccache
addons:
apt:
sources:
- ubuntu-toolchain-r-test
packages:
- libwww-perl
- g++-5
- libubsan0
- parallel
- libc6-dev-i386
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="ccache /usr/bin/g++-5"
- EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"

# OS X using clang++
- stage: Test different OS/CXX/Flags
os: osx
sudo: false
compiler: clang
cache: ccache
before_install:
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
- export PATH=$PATH:/usr/local/opt/ccache/libexec
env: COMPILER="ccache clang++"

# Ubuntu Linux with glibc using g++-5, debug mode
- stage: Test different OS/CXX/Flags
os: linux
sudo: false
compiler: gcc
cache: ccache
addons:
apt:
sources:
- ubuntu-toolchain-r-test
packages:
- libwww-perl
- g++-5
- libubsan0
- libc6-dev-i386
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="ccache /usr/bin/g++-5"
- EXTRA_CXXFLAGS="-DDEBUG"
script: echo "Not running any tests for a debug build."

# Ubuntu Linux with glibc using clang++-3.7, no-debug mode
- stage: Test different OS/CXX/Flags
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
- parallel
- libc6-dev-i386
before_install:
- mkdir bin ; ln -s /usr/bin/gcc-5 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 /usr/bin/clang++-3.7"
- EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DNDEBUG"
- CCACHE_CPP2=yes

# Ubuntu Linux with glibc using clang++-3.7, debug mode, disable USE_DSTRING
- stage: Test different OS/CXX/Flags
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
- libc6-dev-i386
before_install:
- mkdir bin ; ln -s /usr/bin/gcc-5 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 /usr/bin/clang++-3.7"
- EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DDEBUG -DUSE_STD_STRING"
- CCACHE_CPP2=yes
script: echo "Not running any tests for a debug build."

# cmake build using g++-5
- stage: Test different OS/CXX/Flags
os: linux
compiler: gcc
cache: ccache
env:
- BUILD_SYSTEM=cmake
addons:
apt:
sources:
- ubuntu-toolchain-r-test
packages:
- g++-5
- libc6-dev-i386
before_install:
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
install:
- ccache -z
- ccache --max-size=1G
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
- cmake --build build -- -j4
script: (cd build; ctest -V -L CORE -j2)

- stage: Test different OS/CXX/Flags
os: osx
compiler: clang
cache: ccache
before_install:
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
- export PATH=$PATH:/usr/local/opt/ccache/libexec
env:
- BUILD_SYSTEM=cmake
- CCACHE_CPP2=yes
install:
- ccache -z
- ccache --max-size=1G
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
- cmake --build build -- -j4
script: (cd build; ctest -V -L CORE -j2)


# Run Coverity
- stage: Test different OS/CXX/Flags
os: linux
sudo: required
compiler: gcc
cache: ccache
addons:
apt:
sources:
- ubuntu-toolchain-r-test
packages:
- libwww-perl
- g++-5
coverity_scan:
project:
name: "diffblue/cbmc"
description: "Travis build of ${TRAVIS_COMMIT}"
notification_email: "[email protected]"
build_command_prepend: "make -C jbmc/src java-models-library-download"
build_command_prepend: "make -C src minisat2-download"
build_command: "make -C src -j2; make -C jbmc/src -j2"
branch_pattern: "develop"
before_install:
- |
if [[ "${TRAVIS_EVENT_TYPE}" != "cron" ]]
then
echo "This is not a cron build and build is not needed."
travis_terminate 0
fi
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
- sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 90
- g++ --version
# Coverity runs as part of before_script
env:
- NAME="COVERITY_SCAN"
- COMPILER="ccache g++"
script: echo "This is coverity build. No need for tests."

allow_failures:
- <<: *formatting-stage
- <<: *linter-stage
language: generic

install:
- ccache -z
- ccache --max-size=1G
- make -C jbmc/src java-models-library-download
- make -C src minisat2-download
- make -C src/ansi-c library_check
- make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
- make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
- make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
- /bin/true

script:
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
- env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
- make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
- make -C unit test
- env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
- make -C jbmc/unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
- make -C jbmc/unit test

before_cache:
- ccache -s
- /bin/true

notifications:
webhooks:
Expand All @@ -294,3 +16,4 @@ notifications:
on_start: never
on_cancel: never
on_error: always