Merge branch 'develop' into feature/malloc-may-fail

Author: danpoe

.gitignore

@@ -1,6 +1,7 @@
 # Local files generated by IDEs
 .vs/*
 .vscode/*
+*.code-workspace
 ~AutoRecover.*
 *.sln
 *.vcxproj*

.travis.yml

@@ -243,7 +243,7 @@ jobs:
         - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
-      script: (cd build; ctest -V -L CORE -j2)
+      script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2)
 
     # cmake build using clang++-6
     - stage: Test different OS/CXX/Flags
@@ -280,7 +280,7 @@ jobs:
         - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments' '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
-      script: (cd build; ctest -V -L CORE -j2)
+      script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2)
 
     # cmake build on OSX, using default clang
     - stage: Test different OS/CXX/Flags
@@ -300,7 +300,7 @@ jobs:
         - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
-      script: (cd build; ctest -V -L CORE -j2)
+      script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2)
 
 
     # Run Coverity
@@ -338,6 +338,37 @@ jobs:
         - WITH_MEMORY_ANALYZER=1
       script: echo "This is coverity build. No need for tests."
 
+    # cmake install test
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      dist: trusty
+      sudo: false
+      compiler: gcc
+      cache: ccache
+      env:
+        - NAME="cmake install test"
+        - BINARIES="cbmc goto-cc goto-gcc goto-ld goto-instrument goto-analyzer goto-diff goto-harness jbmc janalyzer jdiff"
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - g++-5
+            - maven
+      install:
+        - ccache -z
+        - ccache --max-size=1G
+        - cmake --version
+        - cmake -S . -Bbuild '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5' '-DCMAKE_INSTALL_PREFIX=install'
+        - cmake --build build -- -j4
+        - pushd build; make install; popd
+      script: |
+        for b in $BINARIES; do
+          ( echo === $b === &&
+            install/bin/$b --version &&
+            man -M install/share/man $b | head ) || exit 1 ;
+        done
+
 install:
   - ccache -z
   - ccache --max-size=1G
@@ -355,9 +386,13 @@ script:
   - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
+  - echo "Running expected failure tests"
+  - make TAGS="[!shouldfail]" -C unit test
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
   - make -C jbmc/unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C jbmc/unit test
+  - echo "Running expected failure tests"
+  - make TAGS="[!shouldfail]" -C jbmc/unit test
 
 before_cache:
   - ccache -s

COMPILING.md

@@ -255,6 +255,14 @@ require manual modification of build files.
    to generate IDE projects by supplying the `-G` flag.  Run `cmake -G` for a
    comprehensive list of supported back-ends.
 
+   On macOS >10.14, the build will fail unless you explicitly specify
+   the full path to the compiler. This issue is being tracked
+   [here](https://github.com/diffblue/cbmc/issues/4956). The invocation thus
+   looks like this:
+   ```
+   cmake -S. -Bbuild -DCMAKE_C_COMPILER=/usr/bin/clang
+   ```
+
    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

README.md

@@ -1,6 +1,6 @@
 [![Build Status][travis_img]][travis]
-![Build Status][codebuild_img]
-![Build Status][codebuild_windows_img]
+[![Build Status][codebuild_img]][codebuild]
+[![Build Status][codebuild_windows_img]][codebuild_windows]
 [![Build Status][coverity_img]][coverity]
 [![Build Status][codecov_img]][codecov]
 
@@ -56,7 +56,9 @@ License
 
 [travis]: https://travis-ci.org/diffblue/cbmc
 [travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=master
+[codebuild]: https://us-east-1.console.aws.amazon.com/codesuite/codebuild/projects/cbmc/history?region=us-east-1
 [codebuild_img]: https://codebuild.us-east-1.amazonaws.com/badges?uuid=eyJlbmNyeXB0ZWREYXRhIjoiajhxcmNGUEgyV0xZa2ZFaVd3czJmbm1DdEt3QVdJRVdZaGJuMTUwOHFrZUM3eERwS1g4VEQ3Ymw3bmFncldVQXArajlYL1pXbGZNVTdXdndzUHU4Ly9JPSIsIml2UGFyYW1ldGVyU3BlYyI6IkVUUEdWVEt0SUFONlhyNVAiLCJtYXRlcmlhbFNldFNlcmlhbCI6MX0%3D&branch=develop
+[codebuild_windows]: https://us-east-1.console.aws.amazon.com/codesuite/codebuild/projects/cbmc-windows/history?region=us-east-1
 [codebuild_windows_img]: https://codebuild.us-east-1.amazonaws.com/badges?uuid=eyJlbmNyeXB0ZWREYXRhIjoiTFQ4Q0lCSEc1Rk5NcmlzaFZDdU44Vk8zY0c1VCtIVWMwWnJMRitmVFI5bE94Q3dhekVPMWRobFU2Q0xTTlpDSWZUQ3J1eksrWW1rSll1OExXdll2bExZPSIsIml2UGFyYW1ldGVyU3BlYyI6InpqcloyaEdxbjBiQUtvNysiLCJtYXRlcmlhbFNldFNlcmlhbCI6MX0%3D&branch=develop
 [coverity]: https://scan.coverity.com/projects/diffblue-cbmc
 [coverity_img]: https://scan.coverity.com/projects/13552/badge.svg

buildspec-linux-clang.yml

@@ -27,10 +27,14 @@ phases:
   post_build:
     commands:
       - make -C unit test
+      - echo "Running expected failure tests"
+      - make TAGS="[!shouldfail]" -C unit test
       - make -C regression test CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments'
       - make -C regression/cbmc test-paths-lifo
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
+      - echo "Running expected failure tests"
+      - make TAGS="[!shouldfail]" -C jbmc/unit test
       - make -C jbmc/regression test
       - echo Build completed on `date`
 cache:

buildspec-linux-cmake-gcc.yml

@@ -12,7 +12,7 @@ phases:
     commands:
       - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list
       - apt-get update -y
-      - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq
+      - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq cmake
   build:
     commands:
       - echo Build started on `date`
@@ -22,6 +22,7 @@ phases:
   post_build:
     commands:
       - cd build; ctest -V -L CORE -j2
+      - cd build; ctest -V -R unit-xfail -j2
       - echo Build completed on `date`
 cache:
   paths:

buildspec-windows.yml

@@ -57,6 +57,10 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" '
 
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C unit test BUILD_ENV=MSVC" '
+
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test BUILD_ENV=MSVC" '
@@ -65,6 +69,10 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" '
 
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C jbmc/unit test BUILD_ENV=MSVC" '
+
 cache:
   paths:
     - 'c:\clcache\**\*'

buildspec.yml

@@ -13,7 +13,7 @@ phases:
     commands:
       - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list
       - apt-get update -y
-      - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb
+      - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb libxml2-utils
   build:
     commands:
       - echo Build started on `date`
@@ -26,10 +26,14 @@ phases:
   post_build:
     commands:
       - make -C unit test
+      - echo "Running expected failure tests"
+      - make TAGS="[!shouldfail]" -C unit test
       - make -C regression test
       - make -C regression/cbmc test-paths-lifo
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
+      - echo "Running expected failure tests"
+      - make TAGS="[!shouldfail]" -C jbmc/unit test
       - make -C jbmc/regression test
       - echo Build completed on `date`
 cache:

doc/cprover-manual/goto-harness.md renamed to doc/architectural/goto-harness.md

@@ -16,12 +16,32 @@ to the basic data structures and workflow needed for contributing to
 
 ## Initial setup
 
-Clone the [CBMC repository][cbmc-repo] and build it:
+Clone the [CBMC repository][cbmc-repo] and build it. The build instructions are
+written in a file called COMPILING.md in the top level of the repository. I
+recommend that you build using CMake---this will place all of the CBMC tools in
+a single directory, which you can add to your `$PATH`. For example, if you built
+the codebase with the following two commands at the top level of the repository:
 
-    git clone https://github.com/diffblue/cbmc.git
-    cd cbmc/src
-    make minisat2-download
-    make
+    cmake -DCMAKE_BUILD_TYPE=Debug                  \
+          -DCMAKE_CXX_COMPILER=/usr/bin/clang++     \
+          -DCMAKE_C_COMPILER=/usr/bin/clang         \
+          -B build -S .
+    cmake --build build
+
+then all the CBMC binaries will be built into `build/bin`, and you can run the
+following commands to make CBMC invokable from your terminal.
+
+    # Assuming you cloned CBMC into ~/code
+    export PATH=~/code/cbmc/build/bin:$PATH
+    # Add to your shell's startup configuration file so that you don't have to run that command every time.
+    echo 'export PATH=~/code/cbmc/build/bin:$PATH' >> .bashrc
+
+If you are using Make instead of CMake, the built binaries will be
+scattered throughout the source tree. This tutorial uses the binaries
+`src/cbmc/cbmc`, `src/goto-instrument/goto-instrument`, and
+`src/goto-cc/goto-gcc`, so you will need to add each of those
+directories to your `$PATH`, or symlink to those binaries from a
+directory that is already in your `$PATH`.
 
 Ensure that [graphviz][graphviz] is installed on your system (in
 particular, you should be able to run a program called `dot`).  Install
@@ -30,48 +50,29 @@ particular, you should be able to run a program called `dot`).  Install
     # In the src directory
     doxygen doxyfile
     # View the documentation in a web browser
-    firefox doxy/html/index.html
+    firefox ~/code/cbmc/doc/html/index.html
 
 If you've never used doxygen documentation before, get familiar with the
 layout.  Open the generated HTML page in a web browser; search for the
 class `goto_programt` in the search bar, and jump to the documentation
 for that class; and read through the copious documentation.
 
-The build writes executable programs into several of the source
-directories.  In this tutorial, we'll be using binaries inside the
-`cbmc`, `goto-instrument`, and `goto-cc` directories.  Add these
-directories to your `$PATH`:
-
-    # Assuming you cloned CBMC into ~/code
-    export PATH=~/code/cbmc/src/goto-instrument:~/code/cbmc/src/goto-cc:~/code/cbmc/src/cbmc:$PATH
-    # Add to your shell's startup configuration file so that you don't have to run that command every time.
-    echo 'export PATH=~/code/cbmc/src/goto-instrument:~/code/cbmc/src/goto-cc:~/code/cbmc/src/cbmc:$PATH' >> .bashrc
-
-Optional: install an image viewer that can read images on stdin.
-I use [feh][feh].
-
 [cbmc-repo]:  https://github.com/diffblue/cbmc/
 [doxygen]:    http://www.stack.nl/~dimitri/doxygen/
 [graphviz]:   http://www.graphviz.org/
-[feh]:        https://feh.finalrewind.org/
-
 
 
 ## Whirlwind tour of the tools
 
-CBMC's code is located under the `cbmc` directory.  Even if you plan to
+CBMC's code is located under the `src` directory.  Even if you plan to
 contribute only to CBMC, it is important to be familiar with several
 other of cprover's auxiliary tools.
 
 
 ### Compiling with `goto-cc`
 
-There should be an executable file called `goto-cc` in the `goto-cc`
-directory; make a symbolic link to it called `goto-gcc`:
-
-    cd cbmc/src/goto-cc
-    ln -s "$(pwd)/goto-cc" goto-gcc
-
+If you built using CMake on Unix, you should be able to run the
+`goto-gcc` command.
 Find or write a moderately-interesting C program; we'll call it `main.c`.
 Run the following commands:
 
@@ -102,16 +103,10 @@ structured programming constructs.
 
 Find or write a small C program (2 or 3 functions, each containing a few
 varied statements).  Compile it using `goto-gcc` as above into an object
-file called `main`.  If you installed `feh`, try the following command
-to dump a control-flow graph:
-
-    goto-instrument --dot main | tail -n +2 | dot -Tpng | feh -
-
-If you didn't install `feh`, you can write the diagram to the file and
-then view it:
+file called `main`. You can write the diagram to a file and then view it:
 
-    goto-instrument --dot main | tail -n +2 | dot -Tpng > main.png
-    Now open main.png with an image viewer
+    goto-instrument --dot main.goto | tail -n +2 | dot -Tpng > main.png
+    open main.png
 
 (the invocation of `tail` is used to filter out the first line of
 `goto-instrument` output.  If `goto-instrument` writes more or less
@@ -148,7 +143,7 @@ At some point in that function, there will be a long sequence of `if` statements
 **Task:** Add a `--greet` switch to `goto-instrument`, taking an optional
 argument, with the following behaviour:
 
-    $ goto-instrument --greet main
+    $ goto-instrument --greet main.goto
     hello, world!
     $ goto-instrument --greet Leperina main
     hello, Leperina!