Update from branch 'master' of https://github.com/diffblue/cbmc

Author: peterschrammel

.travis.yml

@@ -1,30 +1,48 @@
 language: cpp
 
-os:
-  - linux
-  - osx
 sudo: required
 
+matrix:
+  include:
+    - os: linux
+      dist: trusty
+      compiler: clang
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            # newer g++ version (also pulls libstdc++)
+            - g++-4.9
+            - libwww-perl
+    - os: linux
+      dist: trusty
+      compiler: gcc
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            # newer g++ version (also pulls libstdc++)
+            - g++-4.9
+            - libwww-perl
+      before_install:
+        - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.9 90
+    - os: osx
+      compiler: clang
+    - os: osx
+      compiler: gcc
+
 addons:
   apt:
     packages:
       - libwww-perl
 
-compiler:
-  - gcc
-  - clang
-
-before_install:
-  - if [ "$(expr substr $(uname -s) 1 5)" == "Linux" ] ; then sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test && sudo apt-get -qq update && sudo apt-get -qq install g++-4.8 gcc-4.8 && sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 90 && sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 90 ; fi
-
-install:
-  - chmod a+x regression/failed-tests-printer.pl
-  - cd src && make minisat2-download
-
 script:
-  - make CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 && cd ../regression && make test
+  - make -C src minisat2-download
+  - make -C src CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 && make -C regression test
 
 matrix:
   include:
     - env: NAME="CPP-LINT"
-      script: cd .. && python scripts/cpplint.py `git diff --name-only master HEAD`
+      script: DIFF=`git diff --name-only master HEAD` && if [ "$DIFF" != "" ]; then python scripts/cpplint.py $DIFF; fi

COMPILING

@@ -38,6 +38,8 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    yum install gcc gcc-c++ flex bison perl-libwww-perl patch
 
+   Note that you need g++ version 4.9 or newer.
+
 1) As a user, get the CBMC source via
 
    git clone https://github.com/diffblue/cbmc cbmc-git

regression/Makefile

@@ -1,4 +1,4 @@
-DIRS = ansi-c cbmc cpp goto-instrument
+DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)

regression/cbmc/Float-to-int1/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+double nondet_double();
+
+int main(void)
+{
+  double d = nondet_double();
+
+  __CPROVER_assume(d < 0x1.0p+63 && d > 0x1.0p+53);
+
+  long long int i = d;
+  double d1 = i;
+
+  assert(d1 != 0x0);
+
+  return 0;
+}
+

regression/cbmc/Float-to-int1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Float-to-int2/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int nondet_int();
+double nondet_double();
+
+int main(void)
+{
+  int i = nondet_int();
+  double di = (double)i;
+  int j = (int)di;
+
+  assert(i == j);
+
+  return 0;
+}
+

regression/cbmc/Float-to-int2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Float-to-int3/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdint.h>
+
+int64_t nondet_int64_t();
+double nondet_double();
+
+int main(void)
+{
+  int64_t i = nondet_int64_t();
+
+  __CPROVER_assume((i & (int64_t)0x7FF) == (int64_t)0);
+  
+  double di = (double)i;
+  int64_t j = (int64_t)di;
+
+  assert(i == j);
+
+  return 0;
+}
+

regression/cbmc/Float-to-int3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/Makefile

@@ -21,9 +21,10 @@ tests.log: ../test.pl
 clean:
 	@for dir in *; do \
                 if [ -d "$$dir" ]; then \
-                        rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
+                        rm -f $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
                 fi; \
-        done;
+  done;
+	rm -f tests.log
 
 show:
 	@for dir in *; do \

regression/goto-instrument-unwind/assert1/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/assert1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 10 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assert2/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/assert2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 9 --unwinding-assertions
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assert3/main.c

@@ -0,0 +1,9 @@
+
+int main()
+{
+  int i;
+  i = 0;
+  do {
+    i++;
+  } while(i < 10);
+}

regression/goto-instrument-unwind/assert3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 10 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assume1/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+  assert(0);
+}

regression/goto-instrument-unwind/assume1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 10
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assume2/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+  assert(0);
+}

regression/goto-instrument-unwind/assume2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 9
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/break-loop1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
-10
+--unwind 10 --partial-loops
+^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/break-loop2/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
-100
+--unwind 100 --partial-loops
+^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/continue-as-loops1/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+  assert(i==10);
+}

regression/goto-instrument-unwind/continue-as-loops1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwind 5 --continue-as-loops
+^Unwinding loop.*iteration 5
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^Unwinding loop.*iteration 6

regression/goto-instrument-unwind/continue-loop1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
-10
+--unwind 10 --partial-loops
+^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/continue-loop2/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
-100
+--unwind 100 --partial-loops
+^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/do-while-loop1/main.c

@@ -0,0 +1,27 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=100;
+  unsigned c=0, i;
+
+  i=1;
+  do
+  {
+    f();
+    c++;
+    i++;
+  } while(i<=n);
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "do-while loop unwind (1)");
+}

regression/goto-instrument-unwind/do-while-loop1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 10 --partial-loops
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/do-while-loop2/main.c

@@ -0,0 +1,28 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=100;
+  
+  const unsigned n=10;
+  unsigned c=0, i;
+
+  i=1;
+  do
+  {
+    f();
+    c++;
+    i++;
+  } while(i<=n);
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "do-while loop unwind (1)");
+
+}

regression/goto-instrument-unwind/do-while-loop2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 100 --partial-loops
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/empty-loop1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
-10
+--unwind 10 --partial-loops
+^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --