Merge branch 'develop' into show_functions_dfs

Author: Daniel Kroening

src/.dir-locals.el renamed to .dir-locals.el

@@ -1,49 +1,28 @@
 language: cpp
 
-matrix:
+jobs:
   include:
 
-    # Alpine Linux with musl-libc using g++
-    - os: linux
-      sudo: required
-      compiler: gcc
-      cache: ccache
-      services:
-        - docker
-      before_install:
-        - docker pull diffblue/cbmc-builder:alpine-0.0.1
-      env:
-        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.1"
-        - COMPILER="ccache g++"
-
-    # OS X using g++
-    - os: osx
-      sudo: false
-      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
-        - ccache -M 1G
-      env: COMPILER=g++
+    - &linter-stage
+      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="CPP-LINT"
+      install:
+      script: scripts/travis_lint.sh
+      before_cache:
 
-    # OS X using clang++
-    - 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
+    - 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
-    - os: linux
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      os: linux
       sudo: false
       compiler: gcc
       cache: ccache
@@ -58,10 +37,11 @@ matrix:
       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"
+      env: COMPILER="ccache 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 +57,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 +86,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,41 +111,74 @@ matrix:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
-    - env: NAME="CPP-LINT"
+    - 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:
-      script: scripts/travis_lint.sh
-      before_cache:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
 
-    - env: NAME="DOXYGEN-CHECK"
+    # Run Coverity
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      sudo: required
+      compiler: gcc
+      cache: ccache
       addons:
         apt:
+          sources:
+            - ubuntu-toolchain-r-test
           packages:
-            - doxygen
-      install:
-      script: scripts/travis_doxygen.sh
-      before_cache:
+            - libwww-perl
+            - g++-5
+        coverity_scan:
+          project:
+            name: "diffblue/cbmc"
+            description: "Travis build of ${TRAVIS_COMMIT}"
+          notification_email: "[email protected]"
+          build_command_prepend: "make -C src minisat2-download"
+          build_command: "make -C src -j2"
+          branch_pattern: "develop"
+      before_install:
+        - |
+          if [[ "${TRAVIS_EVENT_TYPE}" != "cron" ]]
+          then
+            echo "This is not a cron build and build is not needed."
+            travis_terminate 0
+          fi
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+        - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 90
+        - g++ --version
+      # Coverity runs as part of before_script
+      env:
+        - NAME="COVERITY_SCAN"
+        - COMPILER="ccache g++"
+      script: echo "This is coverity build. No need for tests."
 
   allow_failures:
-    - env: NAME="CPP-LINT"
-      install:
-      script: scripts/travis_lint.sh
-      before_cache:
+    - <<: *linter-stage
 
 install:
-  - COMMAND="make -C src minisat2-download" &&
-    eval ${PRE_COMMAND} ${COMMAND}
-  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $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}
+  - 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
 
 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

.travis.yml

@@ -10,6 +10,7 @@
 * GOTO-INSTRUMENT: New option --remove-function-body
 * GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to
   --no-system-headers
+* GOTO-INSTRUMENT: dump-c can output the generated environment via --harness
 
 
 5.7

CHANGELOG

@@ -0,0 +1,43 @@
+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_EXPORT_COMPILE_COMMANDS true)
+
+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)

CMakeLists.txt

@@ -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
 --------------------
 

COMPILING

@@ -1,4 +1,5 @@
 [![Build Status][travis_img]][travis] [![Build Status][appveyor_img]][appveyor]
+[![Build Status][coverity_img]][coverity]
 
 [CProver Wiki](http://www.cprover.org/wiki)
 
@@ -15,11 +16,38 @@ 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.
 
 [travis]: https://travis-ci.org/diffblue/cbmc
 [travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=master
 [appveyor]: https://ci.appveyor.com/project/diffblue/cbmc/
-[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master
+[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master
+[coverity]: https://scan.coverity.com/projects/diffblue-cbmc
+[coverity_img]: https://scan.coverity.com/projects/13552/badge.svg

README.md

@@ -60,19 +60,6 @@ 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
 
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
@@ -109,6 +96,7 @@ test_script:
     rmdir /s /q cbmc-java\classpath1
     rmdir /s /q cbmc-java\jar-file3
     rmdir /s /q cbmc-java\tableswitch2
+    rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
 
     make test

appveyor.yml

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