about summary refs log blame commit diff homepage
path: root/.travis.yml
blob: 5a8a6e45ebc75313665b121357b316422fb5412d (plain) (tree)
1
2
3
4
5
6
7
8
9
10
11
              
             





                                                                                



                                                                               

                                                                              
                                                                               
 
                                      
                               
                                            
                                       
                                  
                                                       
                                                                                                
                                                                                 


                                  
 
                                                                                                                             
 
           
 
                             
                       
                                                                                                                                                        
                                                                                                                                                        
 
                                                                                                                                                                                  
 
                                                                                            
                                                                                                                                                                  
 
                        
                                                                                                                   
 



                                                                                                                                       
                          
                                                                                                                                                                    
 
                                                     
                                                                                                                                      
 
                                            
                                                                                                                                      
                         
                                                                                                                                                     

                                                                                                                                                        
           

                                                                                                                                                                                          
 

             
                         
                                                                                                                                            
 


                                               






                                                                                  



                                                                                                      
                                  
                
                 
                     
          
 
      
              

                                   
               
                                                                               
                                                      
                                                                               
                                
                                                                         
                                                                                                                                                                  









                                                                               
                                                                         
                                             
                                             
                           
                                    
                                                    


                                          

                                 
sudo: required
dist: trusty
language: cpp
compiler:
    # FIXME: For now, building with Clang is disabled because the STP built with
    # it hits an assertion failure during some tests. We should sort this out
    # eventually and file the bug against STP or Clang whichever is appropriate,
    # but for now it is easier to just reduce the number of configs we test
    # anyway.
    # - clang

    - gcc
env:
    ###########################################################################
    # Configurations
    #
    # Each line in the "env" section represents a set of environment variables
    # passed to a build. Thus each line represents a different build
    # configuration.
    ###########################################################################

    # Check a subset of the matrix of:
    #   LLVM  : {3.4, 3.5, 3.6}
    #   SOLVERS : {Z3, STP, STP:Z3, metaSMT}
    #   STP_VERSION   : {2.1.2, master}
    #   METASMT_VERSION : {v4.rc1}
    #   METASMT_DEFAULT : {BTOR, CVC4, STP, YICES2, Z3}
    #   METASMT_BOOST_VERSION : {x.y.z} // e.g. 1.60.0, libboost-dev will be used if unspecified
    #   UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
    #   DISABLE_ASSERTIONS: {0, 1}
    #   ENABLE_OPTIMIZED: {0, 1}
    #   COVERAGE: {0, 1}
    #   USE_TCMALLOC: {0, 1}

    # COVERAGE when set indicates that coverage data should be uploaded to the service, only ONE job should have COVERAGE set

    matrix:

    # TODO: Add Doxygen build

    # Check newer LLVMs
    - LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
    - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
    - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1

    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1

    # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code
    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 ASAN_BUILD=1

    # Test just using Z3
    - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0

    # Test we can build against STP master
    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0

    # Check we can build latest klee-uclibc branch
    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0

    # Test metaSMT support
    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0

    # Check at least one build with Asserts disabled.
    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0

    # Check at least one Debug+Asserts build
    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0

    # Check with TCMALLOC
    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1

    # Coverage build
    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0
    global:
    - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
    - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
    - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg=

matrix:
  include:
    - os: osx
      osx_image: xcode8.3
      env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0

addons:
  apt:
    sources:
    - sourceline: 'ppa:ubuntu-toolchain-r/test'
    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.4 main'
      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.5 main'
      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.6 main'
      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.7 main'
      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
    - sourceline: 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /'
      key_url: 'http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key'
    packages:
    - gcc-4.8
    - g++-4.8
    - libboost-program-options-dev
    - libcap-dev
    - libedit-dev
    - libselinux1-dev
    - cmake
    - lcov

cache:
  ccache: true
  apt: true
  directories:
    - $HOME/Library/Caches/Homebrew
before_install:
    ###########################################################################
    # Set up the locations to get various packages from
    # We assume the Travis image uses Ubuntu 14.04 LTS
    ###########################################################################
    # Update package information
    - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then sudo apt-get update; fi
    - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update && brew tap klee/klee && brew install ccache && export PATH="/usr/local/opt/ccache/libexec:$PATH" ; fi
    ###########################################################################
    # Set up out of source build directory
    ###########################################################################
    - export KLEE_SRC=`pwd`
    - cd ../
    - mkdir build
    - cd build/
    - export BUILD_DIR=`pwd`
    ###########################################################################
    # Install stuff
    ###########################################################################
    # Install LLVM and the LLVM bitcode compiler we require to build KLEE
    - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh
    - ${KLEE_SRC}/.travis/install-tcmalloc.sh
    # Install lit (llvm-lit is not available)
    - sudo pip2 install lit
    # Get SMT solvers
    - ${KLEE_SRC}/.travis/solvers.sh
    # Get needed utlities/libraries for testing KLEE
    - mkdir test-utils/
    - cd test-utils/
    - ${KLEE_SRC}/.travis/testing-utils.sh
    - cd ../
script:
    # Build KLEE and run tests
    - ${KLEE_SRC}/.travis/klee.sh