.travis.yml

language: cpp

jobs:
  include:

    - &formatting-stage
      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
      env: NAME="clang-format"
      addons:
        apt:
          sources:
            - llvm-toolchain-trusty-7
            - ubuntu-toolchain-r-test
          packages:
            - clang-format-7
      install:
      script: |
        clang-format-7 --version
        # build a pathspec that excludes the files in .clang-format-ignore
        while read file ; do EXCLUDES+="':(top,exclude)$file' " ; done < .clang-format-ignore
        MERGE_BASE=$(git merge-base ${TRAVIS_COMMIT_RANGE%...*} ${TRAVIS_COMMIT_RANGE#*...})
        echo "Checking for formatting errors introduced since $MERGE_BASE"
        # use eval so that quotes (as inserted into $EXCLUDES above) are not interpreted as parts of file names
        eval git-clang-format-7 --binary clang-format-7 $MERGE_BASE -- $EXCLUDES
        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"
        DOXYGEN_VERSION: "1.8.16"
      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:
            - cmake
            - google-cloud-sdk
            - graphviz
      cache:
        directories:
          - ${TRAVIS_BUILD_DIR}/doxygen/build/bin
      install:
        - |
          # Build doxygen if it is not in Travis cache
          if ! [ -x doxygen/build/bin/doxygen ]
          then
            scripts/build_doxygen.sh ${DOXYGEN_VERSION}
          fi
        - export PATH="$PATH:${TRAVIS_BUILD_DIR}/doxygen/build/bin"
      script:
        - echo $PATH
        - doxygen --version
        - scripts/run_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
      dist: trusty
      sudo: false
      compiler: gcc
      cache: ccache
      addons:
        apt:
          sources:
            - ubuntu-toolchain-r-test
          packages:
            - libwww-perl
            - g++-5
            - libubsan0
            - parallel
            - jq
            - gdb
      before_install:
        - mkdir bin
        - ln -s /usr/bin/gcc-5 bin/gcc
        - ln -s /usr/bin/g++-5 bin/g++
      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
      env:
        - COMPILER="ccache /usr/bin/g++-5"
        - WITH_MEMORY_ANALYZER=1

    # 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 gdb
        - export PATH=$PATH:/usr/local/opt/ccache/libexec
      env:
        - COMPILER="ccache clang++"
        - WITH_MEMORY_ANALYZER=0

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

    # Ubuntu Linux with glibc using clang++-7, debug mode, disable USE_DSTRING
    - stage: Test different OS/CXX/Flags
      os: linux
      dist: trusty
      sudo: false
      compiler: clang
      cache: ccache
      addons:
        apt:
          sources:
            - ubuntu-toolchain-r-test
            - llvm-toolchain-trusty-7
          packages:
            - libwww-perl
            - g++-5
            - clang-7
            - libstdc++-5-dev
            - libubsan0
            - jq
            - gdb
      before_install:
        - mkdir bin
        - ln -s /usr/bin/gcc-5 bin/gcc
        - ln -s /usr/bin/g++-5 bin/g++
        - export CCACHE_CPP2=yes
      # env: COMPILER=clang++-7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
      env:
        - COMPILER="ccache /usr/bin/clang++-7"
        - EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DDEBUG -DUSE_STD_STRING"
        - CCACHE_CPP2=yes
        - WITH_MEMORY_ANALYZER=1
      script: echo "Not running any tests for a debug build."

    # cmake build using g++-7, enable NAMED_SUB_IS_FORWARD_LIST
    - stage: Test different OS/CXX/Flags
      os: linux
      dist: trusty
      sudo: false
      compiler: gcc
      cache: ccache
      env:
        - BUILD_SYSTEM=cmake
      addons:
        apt:
          sources:
            - ubuntu-toolchain-r-test
          packages:
            - g++-7
            - jq
            - gdb
      before_install:
        - mkdir bin
        - ln -s /usr/bin/gcc-7 bin/gcc
        - ln -s /usr/bin/g++-7 bin/g++
      install:
        - ccache -z
        - ccache --max-size=1G
        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST' '-DWITH_MEMORY_ANALYZER=On'
        - git submodule update --init --recursive
        - cmake --build build -- -j4
      script: (cd build; bin/unit "[core][irept]")

    # cmake build using g++-7, enable CMAKE_USE_CUDD and BDD_GUARDS
    - stage: Test different OS/CXX/Flags
      os: linux
      dist: trusty
      sudo: false
      compiler: gcc
      cache: ccache
      env:
        - BUILD_SYSTEM=cmake
      addons:
        apt:
          sources:
            - ubuntu-toolchain-r-test
          packages:
            - g++-7
            - jq
            - gdb
      before_install:
        - mkdir bin
        - ln -s /usr/bin/gcc-7 bin/gcc
        - ln -s /usr/bin/g++-7 bin/g++
      install:
        - ccache -z
        - ccache --max-size=1G
        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" '-DWITH_MEMORY_ANALYZER=On'
        - git submodule update --init --recursive
        - cmake --build build -- -j4
      script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2)

    # cmake build using clang++-6
    - stage: Test different OS/CXX/Flags
      os: linux
      dist: trusty
      sudo: false
      compiler: clang
      cache: ccache
      env:
        - BUILD_SYSTEM=cmake
      addons:
        apt:
          sources:
            - ubuntu-toolchain-r-test
            - llvm-toolchain-trusty-7
          packages:
            - libwww-perl
            - g++-5
            - clang-7
            - libstdc++-5-dev
            - libubsan0
            - parallel
            - jq
            - gdb
      before_install:
        - mkdir bin
        # Use gcc/g++ 5 for tests, as Clang doesn't work yet
        # See https://github.com/diffblue/cbmc/issues/2370 for details.
        - ln -s /usr/bin/gcc-5 bin/gcc-5
        - ln -s /usr/bin/g++-5 bin/g++-5
      install:
        - ccache -z
        - ccache --max-size=1G
        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments' '-DWITH_MEMORY_ANALYZER=On'
        - git submodule update --init --recursive
        - cmake --build build -- -j4
      script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2)

    # cmake build on OSX, using default 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 gdb
        - export PATH=$PATH:/usr/local/opt/ccache/libexec
      env:
        - BUILD_SYSTEM=cmake
        - CCACHE_CPP2=yes
      install:
        - ccache -z
        - ccache --max-size=1G
        - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
        - git submodule update --init --recursive
        - cmake --build build -- -j4
      script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2)


    # Run Coverity
    - stage: Test different OS/CXX/Flags
      if: type = cron
      os: linux
      dist: trusty
      sudo: false
      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 setup-submodules"
          build_command_prepend: "make -C src minisat2-download"
          build_command: "make -C src -j2; make -C jbmc/src -j2"
          branch_pattern: "develop"
      before_install:
        - 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++"
        - WITH_MEMORY_ANALYZER=1
      script: echo "This is coverity build. No need for tests."

    # cmake install test
    - stage: Test different OS/CXX/Flags
      os: linux
      dist: trusty
      sudo: false
      compiler: gcc
      cache: ccache
      env:
        - NAME="cmake install test"
        - BINARIES="cbmc goto-cc goto-gcc goto-ld goto-instrument goto-analyzer goto-diff goto-harness jbmc janalyzer jdiff"
      addons:
        apt:
          sources:
            - ubuntu-toolchain-r-test
          packages:
            - g++-5
            - maven
      install:
        - ccache -z
        - ccache --max-size=1G
        - cmake --version
        - cmake -S . -Bbuild '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5' '-DCMAKE_INSTALL_PREFIX=install'
        - cmake --build build -- -j4
        - pushd build; make install; popd
      script: |
        for b in $BINARIES; do
          ( echo === $b === &&
            install/bin/$b --version &&
            man -M install/share/man $b | head ) || exit 1 ;
        done

install:
  - ccache -z
  - ccache --max-size=1G
  - make -C jbmc/src setup-submodules
  - make -C src minisat2-download
  - make -C src/ansi-c library_check
  - make -C src/cpp library_check
  - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
  - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3

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
  - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
  - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
  - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
  - make -C unit test
  - echo "Running expected failure tests"
  - make TAGS="[!shouldfail]" -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
  - echo "Running expected failure tests"
  - make TAGS="[!shouldfail]" -C jbmc/unit test

before_cache:
  - ccache -s

notifications:
  webhooks:
    urls:
      - http://dashboard.diffblue.com/api/travis-webhooks
      - https://us-central1-dev-user-joelallred.cloudfunctions.net/trigger-testgen-from-cbmc
    on_success: always
    on_failure: always
    on_start: never
    on_cancel: never
    on_error: always