From 893565f98d346060bf667fb41c7e61bb0473a8fd Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Tue, 23 Feb 2016 19:33:56 +0000
Subject: [PATCH 1/2] Travis CI configuration

Builds for Linux (uses Travis' Ubuntu/Precise) and OS X
---
 .travis.yml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 .travis.yml

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

From 0a1a47f1216e8f7ddd777ee120e26196b4ca7d02 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Tue, 23 Feb 2016 19:42:32 +0000
Subject: [PATCH 2/2] Initial README.md, including Travis-CI information

---
 README.md | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 README.md

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