Initial README.md, including Travis-CI configuration

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6531 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

.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

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