diff --git a/.travis.yml b/.travis.yml index 1485437fe02..6d7c87b854f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -127,6 +127,43 @@ jobs: - cmake --build build -- -j4 script: (cd build; ctest -V -L CORE) + # 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 src minisat2-download" + build_command: "make -C 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: - <<: *linter-stage diff --git a/README.md b/README.md index 8804b2f0b55..df58e355d0b 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ [![Build Status][travis_img]][travis] [![Build Status][appveyor_img]][appveyor] +[![Build Status][coverity_img]][coverity] [CProver Wiki](http://www.cprover.org/wiki) @@ -47,4 +48,6 @@ License [travis]: https://travis-ci.org/diffblue/cbmc [travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=master [appveyor]: https://ci.appveyor.com/project/diffblue/cbmc/ -[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master \ No newline at end of file +[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master +[coverity]: https://scan.coverity.com/projects/diffblue-cbmc +[coverity_img]: https://scan.coverity.com/projects/13552/badge.svg