Merge branch 'develop' into develop-feature_generate_function_bodies

Author: hannes-steffenhagen-diffblue

.travis.yml

@@ -62,11 +62,12 @@ jobs:
             - libwww-perl
             - g++-5
             - libubsan0
+            - parallel
       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"
+        - COMPILER="ccache /usr/bin/g++-5"
         - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
 
     # OS X using g++
@@ -76,10 +77,8 @@ jobs:
       compiler: gcc
       cache: ccache
       before_install:
-          #we create symlink to non-ccache gcc, to be used in tests
-        - 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
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
+        - export PATH=$PATH:/usr/local/opt/ccache/libexec
       env: COMPILER="ccache g++"
 
     # OS X using clang++
@@ -89,10 +88,11 @@ jobs:
       compiler: clang
       cache: ccache
       before_install:
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
-        - export PATH=/usr/local/opt/ccache/libexec:$PATH
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
+        - export PATH=$PATH:/usr/local/opt/ccache/libexec
       env:
-        - COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
+        - COMPILER="ccache clang++"
+        - EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
 
     # Ubuntu Linux with glibc using g++-5, debug mode
@@ -113,7 +113,7 @@ jobs:
         - 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"
+        - COMPILER="ccache /usr/bin/g++-5"
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
@@ -133,16 +133,17 @@ jobs:
             - clang-3.7
             - libstdc++-5-dev
             - libubsan0
+            - parallel
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
         - export CCACHE_CPP2=yes
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
-        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
+        - COMPILER="ccache /usr/bin/clang++-3.7"
+        - EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DNDEBUG"
         - CCACHE_CPP2=yes
-        - EXTRA_CXXFLAGS="-DNDEBUG"
 
-    # Ubuntu Linux with glibc using clang++-3.7, debug mode
+    # Ubuntu Linux with glibc using clang++-3.7, debug mode, disable USE_DSTRING
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -163,14 +164,15 @@ jobs:
         - export CCACHE_CPP2=yes
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
-        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
+        - COMPILER="ccache /usr/bin/clang++-3.7"
+        - EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DDEBUG -DUSE_STD_STRING"
         - CCACHE_CPP2=yes
-        - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
     # cmake build using g++-5
     - stage: Test different OS/CXX/Flags
       os: linux
+      compiler: gcc
       cache: ccache
       env:
         - BUILD_SYSTEM=cmake
@@ -180,19 +182,22 @@ jobs:
             - ubuntu-toolchain-r-test
           packages:
             - g++-5
+      before_install:
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
     - stage: Test different OS/CXX/Flags
       os: osx
+      compiler: clang
       cache: ccache
       before_install:
         - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
-        - export PATH=/usr/local/opt/ccache/libexec:$PATH
+        - export PATH=$PATH:/usr/local/opt/ccache/libexec
       env:
         - BUILD_SYSTEM=cmake
         - CCACHE_CPP2=yes
@@ -250,13 +255,13 @@ install:
   - ccache --max-size=1G
   - make -C src minisat2-download
   - make -C src/ansi-c library_check
-  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
-  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 clobber.dir memory-models.dir
+  - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
+  - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
-  - make -C unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
+  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
+  - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
 
 before_cache:

CODEOWNERS

@@ -46,6 +46,8 @@ src/cpp/ @kroening @tautschnig @peterschrammel
 
 # These files change frequently and changes are low-risk
 
+src/util/irep_ids.def @diffblue/cbmc-developers
+
 unit/ @diffblue/cbmc-developers
 regression/ @diffblue/cbmc-developers
 

buildspec.yml

@@ -0,0 +1,26 @@
+version: 0.2
+
+phases:
+  install:
+    commands:
+      - echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list
+      - apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
+      - apt-get update -y
+      - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache
+      - apt-get install -y openjdk-7-jdk
+      - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
+      - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1
+  build:
+    commands:
+      - echo Build started on `date`
+      - (cd src ; make minisat2-download)
+      - (cd src ; make CXX="ccache g++" -j2)
+      - (cd regression ; make test)
+  post_build:
+    commands:
+      - echo Build completed on `date`
+artifacts:
+  files:
+cache:
+  paths:
+    - '/root/.ccache/**/*'

doc/architectural/cbmc-guide.md

@@ -597,5 +597,5 @@ they are in the code.
 [^2]: Or references, if reference counted data sharing is enabled. It is
     enabled by default; see the `SHARING` macro.
 
-[^3]: When `USE_DSTRING` is enabled (it is by default), this is actually
+[^3]: Unless `USE_STD_STRING` is set, this is actually
 a `dstring` and thus an integer which is a reference into a string table

regression/CMakeLists.txt

@@ -20,25 +20,29 @@ macro(add_test_pl_tests cmdline)
     add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
 endmacro(add_test_pl_tests)
 
-add_subdirectory(ansi-c)
+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
 add_subdirectory(cbmc)
-add_subdirectory(cbmc-cover)
-add_subdirectory(cbmc-cpp)
 add_subdirectory(cbmc-java)
-add_subdirectory(cbmc-java-inheritance)
-add_subdirectory(cpp)
 add_subdirectory(goto-analyzer)
-add_subdirectory(goto-analyzer-taint)
-add_subdirectory(goto-cc-cbmc)
-add_subdirectory(goto-cc-goto-analyzer)
-add_subdirectory(goto-diff)
+add_subdirectory(ansi-c)
+add_subdirectory(jbmc-strings)
 add_subdirectory(goto-instrument)
+add_subdirectory(cpp)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(cbmc-cover)
 add_subdirectory(goto-instrument-typedef)
+add_subdirectory(strings)
+add_subdirectory(invariants)
+add_subdirectory(goto-diff)
+add_subdirectory(test-script)
+add_subdirectory(goto-analyzer-taint)
+add_subdirectory(cbmc-java-inheritance)
 if(NOT WIN32)
   add_subdirectory(goto-gcc)
 endif()
-add_subdirectory(invariants)
-add_subdirectory(jbmc-strings)
-add_subdirectory(strings)
-add_subdirectory(strings-smoke-tests)
-add_subdirectory(test-script)
+add_subdirectory(goto-cc-cbmc)
+add_subdirectory(cbmc-cpp)
+add_subdirectory(goto-cc-goto-analyzer)
+

regression/Makefile

@@ -1,34 +1,62 @@
-DIRS = ansi-c \
-       cbmc \
-       cbmc-cover \
-       cbmc-cpp \
+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
+DIRS = cbmc \
        cbmc-java \
-       cbmc-java-inheritance \
-       cpp \
        goto-analyzer \
-       goto-analyzer-taint \
-       goto-cc-cbmc \
-       goto-cc-goto-analyzer \
-       goto-diff \
-       goto-gcc \
+       ansi-c \
+       jbmc-strings \
        goto-instrument \
+       cpp \
+       strings-smoke-tests \
+       cbmc-cover \
        goto-instrument-typedef \
-       invariants \
        strings \
-       jbmc-strings \
-       strings-smoke-tests \
+       invariants \
+       goto-diff \
        test-script \
+       goto-analyzer-taint \
+       cbmc-java-inheritance \
+       goto-gcc \
+       goto-cc-cbmc \
+       cbmc-cpp \
+       goto-cc-goto-analyzer \
        # Empty last line
 
-# Check for the existence of $dir. Tests under goto-gcc cannot be run on
-# Windows, so appveyor.yml unlinks the entire directory under Windows.
+# Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks
+# the entire directory under Windows. This variable will contain the list
+# of directories that actually exist on the current platform.
+PLATFORM_DIRS = $(wildcard $(DIRS))
+
+# Run all test directories in sequence
+.PHONY: test
 test:
-	@for dir in $(DIRS); do \
-	  if [ -d "$$dir" ]; then \
-	    $(MAKE) -C "$$dir" test || exit 1; \
-	  fi; \
+	@for dir in $(PLATFORM_DIRS); do \
+		$(MAKE) "$$dir" || exit 1; \
 	done;
 
+# Pattern to execute a single test suite directory
+.PHONY: $(PLATFORM_DIRS)
+$(PLATFORM_DIRS):
+	@echo "Running $@..." ;
+	$(MAKE) -C "$@" test || exit 1;
+
+# Run all test directories using GNU Parallel
+.PHONY: test-parallel
+.NOTPARALLEL: test-parallel
+test-parallel:
+	@echo "Building with $(JOBS) jobs"
+	parallel \
+		--halt soon,fail=1 \
+		--tag \
+		--tagstring '{#}:' \
+		--linebuffer \
+		--jobs $(JOBS) \
+		$(MAKE) "{}" \
+		::: $(PLATFORM_DIRS)
+
+
+.PHONY: clean
 clean:
 	@for dir in *; do \
 		if [ -d "$$dir" ]; then \

regression/cbmc-from-CVS/Array_operations1/main.c

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 instanceof1.class
 
 ^EXIT=0$

regression/cbmc-java/instanceof1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 instanceof3.class
 
 ^EXIT=0$

regression/cbmc-java/instanceof3/test.desc

@@ -0,0 +1,9 @@
+public class B {
+    public int y;
+
+    public static java.util.function.Function<Double, Double> dmul = x -> x * 3.1415;
+
+    public void set(int x) {
+        y = x;
+    }
+}

regression/cbmc-java/lambda1/B.class

@@ -0,0 +1,4 @@
+@FunctionalInterface
+interface CustomLambda<T> {
+    boolean is_ok(T t);
+}