Merge develop into Security Scanner Support

.travis.yml

@@ -1,23 +1,61 @@
 language: cpp
 
-matrix:
+jobs:
   include:
 
+    - &linter-stage
+      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="CPP-LINT"
+      install:
+      script: scripts/travis_lint.sh
+      before_cache:
+
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="DOXYGEN-CHECK"
+      addons:
+        apt:
+          packages:
+            - doxygen
+      install:
+      script: scripts/travis_doxygen.sh
+      before_cache:
+
+    # Ubuntu Linux with glibc using g++-5
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      os: linux
+      sudo: false
+      compiler: gcc
+      cache: ccache
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - libwww-perl
+            - g++-5
+            - libubsan0
+      before_install:
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
+      env: COMPILER="ccache g++-5"
+
     # Alpine Linux with musl-libc using g++
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: required
       compiler: gcc
       cache: ccache
       services:
         - docker
       before_install:
-        - docker pull diffblue/cbmc-builder:alpine-0.0.1
+        - docker pull diffblue/cbmc-builder:alpine-0.0.3
       env:
-        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.1"
+        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.3"
         - COMPILER="ccache g++"
 
     # OS X using g++
-    - os: osx
+    - stage: Test different OS/CXX/Flags
+      os: osx
       sudo: false
       compiler: gcc
       cache: ccache
@@ -26,42 +64,24 @@ matrix:
         - mkdir bin ; ln -s /usr/bin/gcc bin/gcc
         - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
         - export PATH=/usr/local/opt/ccache/libexec:$PATH
-        - ccache -M 1G
-      env: COMPILER=g++
+      env: COMPILER="ccache g++"
 
     # OS X using clang++
-    - os: osx
+    - stage: Test different OS/CXX/Flags
+      os: osx
       sudo: false
       compiler: clang
       cache: ccache
       before_install:
         - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
         - export PATH=/usr/local/opt/ccache/libexec:$PATH
-        - ccache -M 1G
       env:
         - COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
 
-    # Ubuntu Linux with glibc using g++-5
-    - os: linux
-      sudo: false
-      compiler: gcc
-      cache: ccache
-      addons:
-        apt:
-          sources:
-            - ubuntu-toolchain-r-test
-          packages:
-            - libwww-perl
-            - g++-5
-            - libubsan0
-      before_install:
-        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
-      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
-      env: COMPILER="g++-5"
-
     # Ubuntu Linux with glibc using g++-5, debug mode
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: gcc
       cache: ccache
@@ -77,12 +97,13 @@ matrix:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env:
-        - COMPILER="g++-5"
+        - COMPILER="ccache g++-5"
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
     # Ubuntu Linux with glibc using clang++-3.7
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: clang
       cache: ccache
@@ -105,7 +126,8 @@ matrix:
         - CCACHE_CPP2=yes
 
     # Ubuntu Linux with glibc using clang++-3.7, debug mode
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: clang
       cache: ccache
@@ -129,27 +151,11 @@ matrix:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
-    - env: NAME="CPP-LINT"
-      install:
-      script: scripts/travis_lint.sh
-      before_cache:
-
-    - env: NAME="DOXYGEN-CHECK"
-      addons:
-        apt:
-          packages:
-            - doxygen
-      install:
-      script: scripts/travis_doxygen.sh
-      before_cache:
-
   allow_failures:
-    - env: NAME="CPP-LINT"
-      install:
-      script: scripts/travis_lint.sh
-      before_cache:
+    - <<: *linter-stage
 
 install:
+  - ccache --max-size=1G
   - COMMAND="make -C src minisat2-download" &&
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C src boost-download" &&

README.md

@@ -15,6 +15,31 @@ and passing the resulting equation to a decision procedure.
 
 For full information see [cprover.org](http://www.cprover.org/cbmc).
 
+Versions
+========
+
+Get the [latest release](https://github.com/diffblue/cbmc/releases)
+* Releases are tested and for production use.
+
+Get the current *develop* version: `git clone https://github.com/diffblue/cbmc.git`
+* Develop versions are not recommended for production use.
+
+Report bugs
+===========
+
+If you encounter a problem please file a bug report:
+* Create an [issue](https://github.com/diffblue/cbmc/issues)
+
+Contributing to the code base
+=============================
+
+1. Fork the repository
+2. Clone the repository `git clone [email protected]:YOURNAME/cbmc.git`
+3. Create a branch from the `develop` branch (default branch)
+4. Make your changes (follow the [coding guidelines](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md))
+5. Push your changes to your branch
+6. Create a Pull Request targeting the `develop` branch
+
 License
 =======
 4-clause BSD license, see `LICENSE` file.

regression/.gitignore

@@ -0,0 +1 @@
+tests.log

regression/Makefile

@@ -2,11 +2,14 @@ DIRS = ansi-c \
        cbmc \
        cpp \
        cbmc-java \
+       cbmc-java-inheritance \
        goto-analyzer \
+       goto-diff \
        goto-instrument \
        goto-instrument-typedef \
-       goto-diff \
        invariants \
+       strings \
+       strings-smoke-tests \
        test-script \
        # Empty last line
 

regression/cbmc-java-inheritance/Makefile

@@ -0,0 +1,38 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

regression/cbmc-java-inheritance/inheritance01/test.desc

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance01/test.java

@@ -0,0 +1,20 @@
+class A
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class B extends A
+{
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    assert(b.toInt()==12345);
+  }
+}

regression/cbmc-java-inheritance/inheritance02/test.desc

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance02/test.java

@@ -0,0 +1,24 @@
+class A
+{
+  protected int toInt()
+  {
+    return 12345;
+  }
+}
+
+class B extends A
+{
+  public void secondary()
+  {
+    assert(toInt()==12345);
+  }
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    b.secondary();
+  }
+}

regression/cbmc-java-inheritance/inheritance03/test.desc

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance03/test.java

@@ -0,0 +1,24 @@
+class Z 
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class A extends Z
+{
+}
+
+class B extends A
+{
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    assert(b.toInt()==12345);
+  }
+}

regression/cbmc-java-inheritance/inheritance04/test.desc

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance04/test.java

@@ -0,0 +1,28 @@
+class A
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class B extends A
+{
+  public int toInt()
+  {
+    return 9999;
+  }
+}
+
+class Z extends B
+{
+}
+
+class test
+{
+  void check()
+  {
+    Z z=new Z();
+    assert(z.toInt()==9999);
+  }
+}

regression/cbmc-java-inheritance/inheritance05/test.desc

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$