From 177a13d19825312803948c35dc3bac5e46db61de Mon Sep 17 00:00:00 2001
From: Vlastimil Zeman <vlastimil.zeman@diffblue.com>
Date: Wed, 30 Aug 2017 13:30:59 +0100
Subject: [PATCH] Add Coverity scan

Coverity scan will run as separate job in second stage. Ii will terminate
itself as soon as possible if build is not triggered by cron. Therefore
it requires to have cron job setup in settings of diffblue/cbmc and
environment variable `COVERITY_SCAN_TOKEN` in the same project settings.
---
 .travis.yml | 37 +++++++++++++++++++++++++++++++++++++
 README.md   |  5 ++++-
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index 1485437fe0..6d7c87b854 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 8804b2f0b5..df58e355d0 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