diff --git a/.travis.yml b/.travis.yml index 47c74f03ad4..2b612fb3152 100644 --- a/.travis.yml +++ b/.travis.yml @@ -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: "coverity-scan@diffblue.com" - 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: @@ -294,3 +16,4 @@ notifications: on_start: never on_cancel: never on_error: always +