diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 00000000000..82ce565d776 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,25 @@ +language: cpp + +os: + - linux + - osx +sudo: required + +addons: + apt: + packages: + - libwww-perl + +compiler: + - gcc + - clang + +before_install: + - if [ "$(expr substr $(uname -s) 1 5)" == "Linux" ] ; then sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test && sudo apt-get -qq update && sudo apt-get -qq install g++-4.8 gcc-4.8 && sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 90 && sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 90 ; fi + +install: + - chmod a+x regression/failed-tests-printer.pl + - cd src && make minisat2-download + +script: + - make CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 && cd ../regression && make test diff --git a/README.md b/README.md new file mode 100644 index 00000000000..5fe827b3a99 --- /dev/null +++ b/README.md @@ -0,0 +1,21 @@ +[![Build Status][build_img]][travis] + +About +===== + +CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, +most of C11 and most compiler extensions provided by gcc and Visual Studio. It +also supports SystemC using Scoot. It allows verifying array bounds (buffer +overflows), pointer safety, exceptions and user-specified assertions. +Furthermore, it can check C and C++ for consistency with other languages, such +as Verilog. The verification is performed by unwinding the loops in the program +and passing the resulting equation to a decision procedure. + +For full information see [cprover.org](http://www.cprover.org/cbmc). + +License +======= +4-clause BSD license, see `LICENSE` file. + +[build_img]: https://travis-ci.org/tautschnig/cbmc.svg?branch=master +[travis]: https://travis-ci.org/tautschnig/cbmc