Merge current cbmc/master into test-gen-support

.travis.yml

@@ -7,30 +7,44 @@ matrix:
     - os: linux
       sudo: required
       compiler: gcc
+      cache: ccache
       services:
         - docker
       before_install:
-        - docker pull diffblue/cbmc-builder:alpine
+        - docker pull diffblue/cbmc-builder:alpine-0.0.1
       env:
-        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc diffblue/cbmc-builder:alpine"
-        - COMPILER=g++
+        - 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
+        - brew install ccache
+        - export PATH=/usr/local/opt/ccache/libexec:$PATH
       env: COMPILER=g++
 
     # OS X using clang++
     - os: osx
       sudo: false
       compiler: clang
-      env: COMPILER=clang++
+      cache: ccache
+      before_install:
+        - brew install ccache
+        - export PATH=/usr/local/opt/ccache/libexec:$PATH
+      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:
@@ -42,12 +56,34 @@ 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="g++-5"
+
+    # Ubuntu Linux with glibc using g++-5, debug mode
+    - 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"
+        - EXTRA_CXXFLAGS="-DDEBUG"
+      script: echo "Not running any tests for a debug build."
 
     # Ubuntu Linux with glibc using clang++-3.7
     - os: linux
       sudo: false
       compiler: clang
+      cache: ccache
       addons:
         apt:
           sources:
@@ -60,19 +96,60 @@ matrix:
             - libubsan0
       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=clang++-3.7
+      env:
+        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
+        - CCACHE_CPP2=yes
 
+    # Ubuntu Linux with glibc using clang++-3.7, debug mode
+    - os: linux
+      sudo: false
+      compiler: clang
+      cache: ccache
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+            - llvm-toolchain-precise-3.7
+          packages:
+            - libwww-perl
+            - clang-3.7
+            - libstdc++-5-dev
+            - libubsan0
+      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"
+        - CCACHE_CPP2=yes
+        - 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:
+
+  allow_failures:
     - env: NAME="CPP-LINT"
-      script: scripts/travis_lint.sh || true
+      install:
+      script: scripts/travis_lint.sh
+      before_cache:
+
+install:
+  - COMMAND="make -C src minisat2-download" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare $EXTRA_CXXFLAGS\" -j2" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
+    eval ${PRE_COMMAND} ${COMMAND}
 
 script:
-  - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="make -C src minisat2-download" &&
-    eval ${PRE_COMMAND} ${COMMAND} &&
-    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND} &&
+  - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
     COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
-    eval ${PRE_COMMAND} ${COMMAND} &&
-    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
     eval ${PRE_COMMAND} ${COMMAND}
+
+before_cache:
+  - ccache -s

CHANGELOG

@@ -1,3 +1,14 @@
+5.8
+===
+
+* GOTO-INSTRUMENT: --reachability-slice can be used with --property to slice
+  down to a single property only.
+* GOTO-INSTRUMENT: New option --list-calls-args
+* GOTO-INSTRUMENT: New option --print-path-lenghts
+* GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
+* GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
+
+
 5.7
 ===
 
@@ -20,6 +31,9 @@
 * GOTO-CC: GCC-style error/warning messages
 * GOTO-CC: New options --native-compiler and --native-linker to select the
   compiler/linker to be used when building combined native/goto object files.
+* CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed
+  ambiguous --show-reachable-properties.
+* CBMC: New option --no-built-in-assertions
 
 
 5.6

COMPILING

@@ -44,12 +44,18 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    git clone https://github.com/diffblue/cbmc cbmc-git
 
-2) On Debian/Ubuntu, do
+2) On Debian, do
 
    cd cbmc-git/src
    make minisat2-download
    make CXX=g++-6
 
+   On Ubuntu, or other distributions with recent g++, do
+
+   cd cbmc-git/src
+   make minisat2-download
+   make
+
    On Redhat/Fedora etc., do
 
    cd cbmc-git/src
@@ -64,7 +70,7 @@ COMPILATION ON SOLARIS 11
 1) As root, get the necessary development tools:
 
    pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
-   pkg install --accept developer/gcc-5
+   pkg install --accept developer/gcc/gcc-c++-5
 
 2) As a user, get the CBMC source via
 
@@ -86,9 +92,6 @@ COMPILATION ON SOLARIS 11
 
    export LD_LIBRARY_PATH=/usr/gcc/4.9/lib
 
-   Do not attempt to compile with gcc-45 that comes with Solaris 11.
-   It will mis-optimize MiniSat2.
-
 
 COMPILATION ON FREEBSD 11
 -------------------------
@@ -163,23 +166,21 @@ Follow these instructions:
    The patch removes the dependency on zlib and prevents a problem
    with a header file that is often unavailable on Windows.
 
-2) Adjust src/config.inc for the paths to item 1).
-
-3A) To compile with Cygwin, install the mingw compilers, and adjust
+2A) To compile with Cygwin, install the mingw compilers, and adjust
    the second line of config.inc to say
 
    BUILD_ENV = MinGW
 
-3B) To compile with Visual Studio, make sure you have at least Visual
+2B) To compile with Visual Studio, make sure you have at least Visual
    Studio version 12 (2013), and adjust the second line of config.inc to say
 
    BUILD_ENV = MSVC
 
-   Open the Visual Studio Command prompt, and then run the make.exe
-   from Cygwin from in there.
+   Open the Visual Studio Command prompt, and then bash.exe -login from
+   Cygwin from in there. 
+
+3) Type cd src; make - that should do it.
 
-4) Type cd src; make - that should do it.
-   Note that "nmake" is not expected to work. Use "make".
 
 (Optional) A Visual Studio project file can be generated with the script
 "generate_vcxproj" that is in the subdirectory "scripts".  The project file

doc/html-manual/cover.shtml

@@ -149,7 +149,7 @@ To demonstrate the automatic test suite generation in CBMC,
 we call the following command and we are going to explain the command line options one by one.
 </p>
 
-<pre><code>cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
+<pre><code>cbmc pid.c --cover mcdc --unwind 6 --xml-ui
 </code></pre>
 
 <p class="justified">
@@ -173,18 +173,22 @@ pprz >= (float)0 && pprz <= (float)(16 * 600)     id="climb_pid_run.coverage.3"
 
 <p class="justified">
 The "id" of each coverage goal is automatically assigned by CBMC.  For every
-coverage goal, a trace (if there exists) of the program execution that
-satisfies such a goal is printed out in XML format, as the parameters
-<code>--trace --xml-ui</code> are given.  Multiple coverage goals can share a
-trace, when the corresponding execution of the program satisfies all these
-goals at the same time.  Each trace corresponds to a test case. 
+coverage goal, a test suite (if there exists) that <!-- the program execution that-->
+satisfies such a goal is printed out in XML format, as the parameter
+<code>--xml-ui</code> is given.  Multiple coverage goals can share a
+test suite, when the corresponding execution of the program satisfies all these
+goals at the same time.  <!--Each trace corresponds to a test case.-->
 </p>
 
 <p class="justified">
 In the end, the following test suites are automatically generated for testing the PID controller.
 A test suite consists of a sequence of input parameters that are
 passed to the PID function <code>climb_pid_run</code> at each loop iteration. 
 For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
+The complete output from CBMC is in
+<a href="pid_test_suites.xml">pid_test_suites.xml</a>, where every test suite and the coverage goals it is for
+are clearly described.
+
 <pre><code>Test suite:
 Test 1. 
   (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f