Merge pull request diffblue#191 from diffblue/pull-support-20170914

Pull support 20170914

Author: smowton

.travis.yml

@@ -13,7 +13,7 @@ jobs:
       before_cache:
 
     - &doxygen-stage
-      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
       env: NAME="DOXYGEN-CHECK"
       addons:
         apt:
@@ -42,22 +42,6 @@ jobs:
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env: COMPILER="ccache g++-5"
 
-# LOCAL CHANGES: Upgraded to diffblue-builder:alpine-0.0.4 because it includes Python
-
-    # Alpine Linux with musl-libc using g++
-    - stage: Test different OS/CXX/Flags
-      os: linux
-      sudo: required
-      compiler: gcc
-      cache: ccache
-      services:
-        - docker
-      before_install:
-        - docker pull diffblue/diffblue-builder:alpine-0.0.4
-      env:
-        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/diffblue-builder:alpine-0.0.4"
-        - COMPILER="ccache g++"
-
 # LOCAL CHANGES: Added 'ant' to the OSX package list (needed by security-scanner regression tests)
 
     # OS X using g++
@@ -158,40 +142,57 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - g++-5
+      install:
+        - cmake -Hcbmc -Bcbmc/build '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake --build cbmc/build -- -j4
+      script: (cd cbmc/build; ctest -V -L CORE)
+
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+        - CCACHE_CPP2=yes
+      install:
+        - cmake -Hcbmc -Bcbmc/build '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake --build cbmc/build -- -j4
+      script: (cd cbmc/build; ctest -V -L CORE)
+
+
   allow_failures:
     - <<: *linter-stage
-    - <<: *doxygen-stage
 
 # LOCAL CHANGES: added cbmc/ prefix to some of the following commands
 # LOCAL CHANGES: added goto-analyzer.dir, goto-diff.dir and goto-cc.dir to the additional build list (needed for CBMC's regression tests, but not by the security-scanner product)
 
 install:
   - ccache --max-size=1G
-  - COMMAND="make -C cbmc/src minisat2-download" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C cbmc/src boost-download" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C cbmc/src/ansi-c library_check" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C cbmc/src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 goto-analyzer.dir goto-cc.dir goto-diff.dir clobber.dir memory-models.dir musketeer.dir" &&
-    eval ${PRE_COMMAND} ${COMMAND}
+  - make -C cbmc/src minisat2-download
+  - make -C cbmc/src boost-download
+  - make -C cbmc/src/ansi-c library_check
+  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j2
+  - make -C cbmc/src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 goto-analyzer.dir goto-cc.dir goto-diff.dir clobber.dir memory-models.dir
 
 # LOCAL CHANGES: Added cbmc/ prefix, and added unit and regression tests to the end of the list.
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C cbmc/regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C cbmc/unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C cbmc/unit test" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C unit test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\"" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="scripts/travis_run_regression_tests.sh" &&
-    eval ${PRE_COMMAND} ${COMMAND}
+  - env UBSAN_OPTIONS=print_stacktrace=1 make -C cbmc/regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}"
+  - make -C cbmc/unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
+  - make -C cbmc/unit test
+  - make -C unit test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}"
+  - scripts/travis_run_regression_tests.sh
 
 before_cache:
   - ccache -s

cbmc/.travis.yml

@@ -39,20 +39,6 @@ jobs:
       # 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++
-    - 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.3
-      env:
-        - 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++
     - stage: Test different OS/CXX/Flags
       os: osx
@@ -151,29 +137,50 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - g++-5
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+        - CCACHE_CPP2=yes
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+
   allow_failures:
     - <<: *linter-stage
 
 install:
   - ccache --max-size=1G
-  - COMMAND="make -C src minisat2-download" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src boost-download" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src/ansi-c library_check" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&
-    eval ${PRE_COMMAND} ${COMMAND}
+  - make -C src minisat2-download
+  - make -C src boost-download
+  - make -C src/ansi-c library_check
+  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j2
+  - make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 clobber.dir memory-models.dir
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C unit test" && eval ${PRE_COMMAND} ${COMMAND}
+  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}"
+  - make -C unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
+  - make -C unit test
 
 before_cache:
   - ccache -s

cbmc/CMakeLists.txt

@@ -0,0 +1,41 @@
+cmake_minimum_required(VERSION 3.2)
+
+find_program(CCACHE_PROGRAM ccache)
+if(CCACHE_PROGRAM)
+    set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
+    message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
+ endif()
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
+
+include(GNUInstallDirs)
+
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+   "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+)
+    #   Ensure NDEBUG is not set for release builds
+    set(CMAKE_CXX_FLAGS_RELEASE "-O2")
+    #   Enable lots of warnings
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
+elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    #   This would be the place to enable warnings for Windows builds, although
+    #   config.inc doesn't seem to do that currently
+endif()
+
+set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
+
+set(sat_impl "minisat2" CACHE STRING
+    "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
+)
+
+add_subdirectory(src)
+
+if(${enable_cbmc_tests})
+    enable_testing()
+endif()
+add_subdirectory(unit)
+add_subdirectory(regression)

cbmc/COMPILING

@@ -171,7 +171,7 @@ Follow these instructions:
    BUILD_ENV = MSVC
 
    Open the Visual Studio Command prompt, and then bash.exe -login from
-   Cygwin from in there. 
+   Cygwin from in there.
 
 3) Type cd src; make - that should do it.
 
@@ -183,6 +183,53 @@ can be used for building with MSBuild.  Note that you still need to run
 flex/bison using "make generated_files" before opening the project.
 
 
+WORKING WITH CMAKE (EXPERIMENTAL)
+---------------------------------
+
+There is an experimental build based on CMake instead of hand-written
+makefiles. It should work on a wider variety of systems than the standard
+makefile build, and can integrate better with IDEs and static-analysis tools.
+
+0) Run `cmake --version`. If you get a command-not-found error, or the installed
+   version is lower than 3.2, go and install a new version. Most Linux
+   distributions have a package for CMake, and Mac users can get it through
+   Homebrew.  Windows users should download it manually from cmake.org.
+
+1) Create a directory to store your build:
+   `mkdir build`
+   Run this from the *top level* folder of the project. This is different from
+   the other builds, which require you to `cd src` first.
+
+2) Generate build files with CMake:
+   `cmake -H. -Bbuild`
+   This command tells CMake to use the configuration in the current directory,
+   and to generate build files into the `build` directory.
+   This is the point to specify custom build settings, such as compilers and
+   build back-ends. You can use clang (for example) by adding the argument
+   `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell
+   CMake to generate IDE projects by supplying the `-G` flag.
+   Run `cmake -G` for a comprehensive list of supported back-ends.
+
+   Generally it is not necessary to manually specify individual compiler or
+   linker flags, as CMake defines a number of "build modes" including Debug
+   and Release modes. To build in a particular mode, add the flag
+   `-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation.
+
+   If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
+   `-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
+   sanitizers.
+
+   Finally, to enable building universal binaries on macOS, you can pass the
+   flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
+   the build will just be for the architecture of your machine.
+
+3) Run the build:
+   `cmake --build build`
+   This command tells CMake to invoke the correct tool to run the build in the
+   `build` directory. You can also use the build back-end directly by invoking
+   `make`, `ninja`, or opening the generated IDE project as appropriate.
+
+
 WORKING WITH ECLIPSE
 --------------------
 

cbmc/appveyor.yml

@@ -60,19 +60,21 @@ build_script:
 test_script:
 - cmd: |
     cd regression
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" ansi-c/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" cpp/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument/chain.sh
-    sed -i "15s/.*/$goto_cc $name.c/" goto-instrument/chain.sh
-    sed -i "16i mv $name.exe $name.gb" goto-instrument/chain.sh
-    sed -i "23s/.*/  $goto_cc ${name}-mod.c/" goto-instrument/chain.sh
-    sed -i "24i   mv ${name}-mod.exe $name-mod.gb" goto-instrument/chain.sh
-    cat goto-instrument/chain.sh
 
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument-typedef/chain.sh || true
-    sed -i "12s/.*/$GC $NAME.c --function fun/" goto-instrument-typedef/chain.sh || true
-    sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
-    cat goto-instrument-typedef/chain.sh || true
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-cbmc/chain.sh || true
+    sed -i "11s/.*/$GC $NAME.c/" goto-cc-cbmc/chain.sh || true
+    sed -i "12i mv $NAME.exe $NAME.gb" goto-cc-cbmc/chain.sh || true
+    cat goto-cc-cbmc/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-goto-analyzer/chain.sh || true
+    cat goto-cc-goto-analyzer/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-symex/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-symex/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-symex/chain.sh || true
+    cat goto-cc-symex/chain.sh || true
 
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
@@ -111,6 +113,11 @@ test_script:
     rmdir /s /q cbmc-java\tableswitch2
     rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
+    rmdir /s /q symex\va_args_10
+    rmdir /s /q symex\va_args_2
+    rmdir /s /q symex\va_args_3
+    rmdir /s /q symex\va_args_5
+    rmdir /s /q symex\va_args_6
 
     make test
 

cbmc/regression/CMakeLists.txt

@@ -0,0 +1,36 @@
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
+set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
+
+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND ${test_pl_path} -c ${cmdline} ${flag}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile}"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests name cmdline)
+    add_test_pl_profile("${name}" "${cmdline}" -C CORE)
+    add_test_pl_profile("${name}" "${cmdline}" -T THOROUGH)
+    add_test_pl_profile("${name}" "${cmdline}" -F FUTURE)
+    add_test_pl_profile("${name}" "${cmdline}" -K KNOWNBUG)
+endmacro(add_test_pl_tests)
+
+add_subdirectory(ansi-c)
+add_subdirectory(cbmc)
+add_subdirectory(cbmc-java)
+add_subdirectory(cbmc-java-inheritance)
+add_subdirectory(cpp)
+add_subdirectory(goto-analyzer)
+add_subdirectory(goto-diff)
+add_subdirectory(goto-instrument)
+add_subdirectory(goto-instrument-typedef)
+add_subdirectory(invariants)
+add_subdirectory(strings)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(test-script)