Security scanner support

.travis.yml

@@ -77,4 +77,8 @@ script:
     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} &&
+    COMMAND="make -C src clean" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}

CHANGELOG

@@ -1,3 +1,99 @@
+5.7
+===
+
+* General: All tools now support the same set of --*-check options.
+* General: Added --conversion-check to catch type casts that cause loss of
+  information. Previously --(un)signed-overflow-check would report these.
+* CBMC: New option --symex-coverage-report to produce a Cobertura-compatible
+  statement- and branch coverage report.
+* CBMC/Java: New options --java-max-vla-length, --java-unwind-enum-static,
+  --java-cp-include-files, --lazy-methods.
+* GOTO-INSTRUMENT: Static loop unwinding via --unwind or via new options
+  --unwindset, --unwindset-file, --unwinding-assertions, --partial-loops,
+  --continue-as-loops, --log
+* GOTO-INSTRUMENT: New option --slice-global-inits
+* GOTO-INSTRUMENT: Inlining via --inline, --partial-inline, --function-inline,
+  --no-caching
+* GOTO-INSTRUMENT: New options --remove-function-pointers, --model-argc-argv,
+  --show-threaded
+* GOTO-CC: Additional drop-in replacement support for bcc, as, as86
+* 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
+===
+
+Bugfixes in the C, C++, Java front-ends.
+
+
+5.5
+===
+
+This is a major release, with significant changes. The option
+--all-properties is now the default; to restore the previous behaviour,
+use --stop-on-fail. The primary area of attention was again the Java
+front-end. We have furthermore added test-suite generation for branch
+coverage, location coverage, condition coverage, decision coverage and
+MC/DC.
+
+
+5.4
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+area of attention was again the Java front-end. We have also updated to
+Minisat 2.2.1.
+
+
+5.3
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+area of attention is the Java front-end.
+
+
+5.2
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+areas of attention are the full slicer, the Java frontend, test suite
+generation and support for the Glucose solver.
+
+
+5.1
+===
+
+This is a minor release, focused primarily on maintenance. Support for solving
+floating-point problems using for SMT-LIB2 solvers without support for the
+floating-point theory has been added.
+
+
+5.0
+===
+
+This is a major release, focused primarily on performance improvements.
+Furthermore, the support for the floating-point theory for SMT-LIB2 has been
+improved substantially. This release breaks compatibility with the goto-binary
+format used by earlier releases; i.e., you will need to rebuild your
+goto-binaries.
+
+
+4.9
+===
+
+This release is primarily for maintenance purposes and does not add any major
+new features. The support for SMT-LIB2 solvers has been improved substantially.
+
+
+4.8
+===
+
+
 4.7
 ===
 

COMPILING

@@ -36,18 +36,31 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    On Red Hat/Fedora or derivates, do
 
-   yum install gcc gcc-c++ flex bison perl-libwww-perl patch
+   yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
 
    Note that you need g++ version 5.2 or newer.
 
 1) As a user, get the CBMC source via
 
    git clone https://github.com/diffblue/cbmc cbmc-git
 
-2) 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
+   make minisat2-download
+   scl enable devtoolset-6 bash
    make
 
 
@@ -57,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
 
@@ -79,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
 -------------------------
@@ -156,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