Merge pull request #941 from thk123/update-to-master-19-05-17

Update test-gen-support from master

Author: smowton

.travis.yml

@@ -145,13 +145,16 @@ install:
     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 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
+  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&
     eval ${PRE_COMMAND} ${COMMAND}
 
 script:
   - 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 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}
 
 before_cache:
   - ccache -s

CODING_STANDARD

@@ -26,23 +26,23 @@ Whitespaces:
 - No whitespaces in blank lines
 - Put argument lists on next line (and ident 2 spaces) if too long
 - Put parameters on separate lines (and ident 2 spaces) if too long
-- No whitespaces around colon for inheritance, 
+- No whitespaces around colon for inheritance,
   put inherited into separate lines in case of multiple inheritance
 - The initializer list follows the constructor without a whitespace
   around the colon. Break line after the colon if required and indent members.
 - if(...), else, for(...), do, and while(...) are always in a separate line
-- Break expressions in if, for, while if necessary and align them 
+- Break expressions in if, for, while if necessary and align them
   with the first character following the opening parenthesis
 - Use {} instead of ; for the empty statement
-- Single line blocks without { } are allowed, 
+- Single line blocks without { } are allowed,
   but put braces around multi-line blocks
-- Use blank lines to visually separate logically cohesive code blocks 
+- Use blank lines to visually separate logically cohesive code blocks
   within a function
 - Have a newline at the end of a file
 
 Comments:
 - Do not use /* */ except for file and function comment blocks
-- Each source and header file must start with a comment block 
+- Each source and header file must start with a comment block
   stating the Module name and Author [will be changed when we roll out doxygen]
 - Each function in the source file (not the header) is preceded
   by a function comment header consisting of a comment block stating
@@ -75,9 +75,9 @@ Comments:
 - Use #ifdef DEBUG to guard debug code
 
 Naming:
-- Identifiers may use the characters [a-z0-9_] and should start with a 
+- Identifiers may use the characters [a-z0-9_] and should start with a
   lower-case letter (parameters in constructors may start with _).
-- Use american spelling for identifiers. 
+- Use american spelling for identifiers.
 - Separate basic words by _
 - Avoid abbreviations (e.g. prefer symbol_table to of st).
 - User defined type identifiers have to be terminated by 't'. Moreover,
@@ -122,7 +122,7 @@ Program Command Line Options
   from the command line into the options
 
 C++ features:
-- Do not use namespaces.
+- Do not use namespaces, except for anonymous namespaces.
 - Prefer use of 'typedef' insted of 'using'.
 - Prefer use of 'class' instead of 'struct'.
 - Write type modifiers before the type specifier.
@@ -136,7 +136,7 @@ C++ features:
 - Avoid iterators, use ranged for instead
 - Avoid allocation with new/delete, use unique_ptr
 - Avoid pointers, use references
-- Avoid char *, use std::string 
+- Avoid char *, use std::string
 - For numbers, use int, unsigned, long, unsigned long, double
 - Use mp_integer, not BigInt
 - Use the functions in util for conversions between numbers and strings
@@ -146,13 +146,13 @@ C++ features:
 - Use instances of std::size_t for comparison with return values of .size() of
   STL containers and algorithms, and use them as indices to arrays or vectors.
 - Do not use default values in public functions
-- Use assertions to detect programming errors, e.g. whenever you make 
+- Use assertions to detect programming errors, e.g. whenever you make
   assumptions on how your code is used
-- Use exceptions only when the execution of the program has to abort 
+- Use exceptions only when the execution of the program has to abort
   because of erroneous user input
-- We allow to use 3rd-party libraries directly. 
-  No wrapper matching the coding rules is required. 
-  Allowed libraries are: STL. 
+- We allow to use 3rd-party libraries directly.
+  No wrapper matching the coding rules is required.
+  Allowed libraries are: STL.
 - When throwing, omit the brackets, i.e. `throw "error"`.
 - Error messages should start with a lower case letter.
 - Use the auto keyword if and only if one of the following
@@ -165,12 +165,30 @@ Architecture-specific code:
 - Don't include architecture-specific header files without #ifdef ...
 
 Output:
-- Do not output to cout or cerr directly (except in temporary debug code, 
+- Do not output to cout or cerr directly (except in temporary debug code,
   and then guard #include <iostream> by #ifdef DEBUG)
 - Derive from messaget if the class produces output and use the streams provided
   (status(), error(), debug(), etc)
 - Use '\n' instead of std::endl
 
+Unit tests:
+ - Unit tests are written using Catch: https://github.com/philsquared/Catch/
+ - For large classes:
+    - Create a separate file that contains the tests for each method of each
+      class
+    - The file should be named according to
+      `unit/class/path/class_name/function_name.cpp`
+ - For small classes:
+    - Create a separate file that contains the tests for all methods of each
+      class
+    - The file should be named according to unit/class/path/class_name.cpp
+ - Catch supports tagging, tests should be tagged with all the following tags:
+    - [core] should be used for all tests unless the test takes more than 1
+      second to run, then it should be tagged with [long]
+    - [folder_name] of the file being tested
+    - [class_name] of the class being tested
+    - [function_name] of the function being tested
+
 You are allowed to break rules if you have a good reason to do so.
 
 Pre-commit hook to run cpplint locally

COMPILING

@@ -38,7 +38,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
 
-   Note that you need g++ version 5.2 or newer.
+   Note that you need g++ version 4.9 or newer.
 
 1) As a user, get the CBMC source via
 

appveyor.yml

@@ -54,7 +54,7 @@ build_script:
     cp -r deps/minisat2-2.2.1 minisat-2.2.1
     patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch
     call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64
-    sed -i "s/BUILD_ENV.*/BUILD_ENV = MSVC/" src/config.inc
+    sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc
     make -C src -j2
 
 test_script:
@@ -108,3 +108,7 @@ test_script:
     rmdir /s /q goto-instrument\slice08
 
     make test
+
+    cd ..
+    make -C unit all
+    make -C unit test

doc/html-manual/api.shtml

@@ -111,11 +111,14 @@ void __CPROVER_cover(_Bool condition);
 </code>
 <hr>
 
+<p>This statement defines a custom coverage criterion, for usage
+with the <a href="cover.shtml">test suite generation feature</a>.</p>
+
 <p class="justified">
 </p>
 
-<h4>__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isfinite,
-__CPROVER_isfinite, __CPROVER_sign</h4>
+<h4>__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isinf,
+__CPROVER_isnormal, __CPROVER_sign</h4>
 
 <hr>
 <code>

doc/html-manual/cover.shtml

@@ -10,8 +10,6 @@
 
 <h3>A Small Tutorial with A Case Study</h3>
 
-<!--<h4>Verilog vs. ANSI-C</h4>-->
-
 <p class="justified">
 We assume that CBMC is installed on your system. If not so, follow
 <a href="installation-cbmc.shtml">these instructions</a>.</p>
@@ -238,4 +236,42 @@ coverage criteria like <code>branch</code>, <code>decision</code>,
 <code>path</code> etc.  are also available when calling CBMC.
 </p>
 
+<h3>Coverage Criteria</h3>
+
+<p class="justified">
+The table below summarizes the coverage criteria that CBMC supports.
+</p>
+
+<table class="fancy">
+
+<tr><th>Criterion</th><th>Definition</th></tr>
+
+<tr><td>assertion</td>
+<td>For every assertion, generate a test that reaches it</td></tr>
+
+<tr><td class="alt">location</td>
+<td class="alt">For every location, generate a test that reaches it</td></tr>
+
+<tr><td>branch</td>
+<td>Generate a test for every branch outcome</td></tr>
+
+<tr><td class="alt">decision</td>
+<td class="alt">Generate a test for both outcomes of every Boolean expression
+that is not an operand of a propositional connective</td></tr>
+
+<tr><td>condition</td>
+<td>Generate a test for both outcomes of every Boolean expression</td></tr>
+
+<tr><td class="alt">mcdc</td>
+<td class="alt">Modified Condition/Decision Coverage (MC/DC)</td></tr>
+
+<tr><td>path</td>
+<td>Bounded path coverage</td></tr>
+
+<tr><td class="alt">cover</td>
+<td class="alt">Generate a test for every <code>__CPROVER_cover</code> statement
+</td></tr>
+
+</table>
+
 <!--#include virtual="footer.inc" -->

doc/html-manual/modeling-nondet.shtml

@@ -39,9 +39,8 @@ prefix <code>nondet_</code>. As an example, the following function
 returns a nondeterministically chosen unsigned short int:
 </p>
 
-<code>
-unsigned short int nondet_ushortint();
-</code>
+<pre><code class="c">unsigned short int nondet_ushortint();
+</code></pre>
 
 <p class="justified">Note that the body of the function is not defined.  The
 name of the function itself is irrelevant (save for the prefix), but must be

pkg/arch/PKGBUILD

@@ -0,0 +1,40 @@
+# Maintainer: Vlastimil Zeman <vlastimil.zeman@diffblue.com>
+
+pkgname=cbmc
+pkgver=5.7
+pkgrel=1
+pkgdesc="Bounded Model Checker for C and C++ programs"
+arch=("x86_64")
+url="https://github.com/diffblue/cbmc"
+license=("BSD-4-Clause")
+depends=("gcc-libs>=6.3")
+makedepends=("gcc>=6.3"
+             "make>=4.2"
+             "patch>=2.7"
+             "perl-libwww>=6.24"
+             "bison>=3.0"
+             "flex>=2.6")
+source=("https://github.com/diffblue/cbmc/archive/$pkgname-$pkgver.tar.gz")
+sha256sums=("4f98cdce609532d3fc2587299ee4a6544f63aff5cf42e89d2baaa3d3562edf3e")
+
+
+build() {
+        make -C "$pkgname-$pkgname-$pkgver/src" minisat2-download
+        make -C "$pkgname-$pkgname-$pkgver/src" -j$(getconf _NPROCESSORS_ONLN)
+}
+
+
+check() {
+        make -C "$pkgname-$pkgname-$pkgver/regression" test
+}
+
+
+package() {
+        mkdir -p "$pkgdir/usr/bin/"
+        for binary in $pkgname goto-analyzer goto-cc goto-diff goto-instrument
+        do
+                cp "$pkgname-$pkgname-$pkgver/src/$binary/$binary" "$pkgdir/usr/bin/"
+                chmod 755 "$pkgdir/usr/bin/$binary"
+                chown root:root "$pkgdir/usr/bin/$binary"
+        done
+}

pkg/arch/README.md

@@ -0,0 +1,17 @@
+# Arch Linux Package
+
+Update packages and install build dependencies
+
+```bash
+sudo pacman -Sy archlinux-keyring && sudo pacman -Syyu
+sudo pacman -S gcc bison flex make patch perl-libwww fakeroot
+```
+
+Create folder for package and copy [PKGBUILD](PKGBUILD) file there.
+
+Build package by running `makepkg` in that folder. That will compile *CBMC* and
+run all tests. To install package run
+
+```bash
+sudo pacman -U cbmc-5.7-1-x86_64.pkg.tar.xz`
+```

regression/cbmc-cover/built-ins1/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --unwind 1
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 7 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins2/main.c

@@ -0,0 +1,19 @@
+struct mystruct {
+  int x;
+  char y;
+};
+
+int main()
+{
+  struct mystruct s;
+  char c;
+  __CPROVER_input("c", c);
+
+  memset(&s,c,sizeof(struct mystruct));
+
+  if(s.y=='A')
+  {
+    return 0;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins3/main.c

@@ -0,0 +1,14 @@
+#include <stdio.h>
+
+int main()
+{
+  const char *s="test";
+  int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
+
+  if(ret<0)
+  {
+    return 1;
+  }
+
+  return 0;
+}

regression/cbmc-cover/built-ins3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins4/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}