Merge pull request #705 from peterschrammel/pull-from-master

Update test-gen-support

Author: forejtv

CHANGELOG

@@ -1,3 +1,96 @@
+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.
+
+
+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,25 @@ 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/Ubuntu, do
 
    cd cbmc-git/src
    make minisat2-download
+   make CXX=g++-6
+
+   On Redhat/Fedora etc., do
+
+   cd cbmc-git/src
+   make minisat2-download
+   scl enable devtoolset-6 bash
    make
 
 

regression/cbmc-java/multinewarray/multinewarray.class

@@ -12,8 +12,8 @@ public static void main(String[] args)
     assert some_a[0].length==3;
     assert some_a[0][0].length==2;
 
-    int x=10;
-    int y=20;
+    int x=3;
+    int y=5;
     int[][] int_array = new int[x][y];
 
     for(int i=0; i<x; ++i)

regression/cbmc-java/multinewarray/multinewarray.java

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 multinewarray.class
 
 ^EXIT=0$

regression/cbmc-java/multinewarray/test.desc

@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
-
 ^\*\* 2 of 6 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-assertion/test.desc

@@ -6,6 +6,5 @@ main.c
 ^\[main.assertion.2\] assertion y: FAILURE$
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
-
 ^\*\* 1 of 4 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-assignment/test.desc

@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$
 ^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
 ^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-copy/test.desc

@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] success 1: SUCCESS$
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
-
 ^\*\* 3 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-if/test.desc

@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
 ^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-initialisation/test.desc

@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
-
 ^\*\* 1 of 5 failed \(2 iterations\)$
 ^VERIFICATION FAILED$

regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -2,6 +2,5 @@ CORE
 main.c
 
 ^\*\* Results:$
-
 ^\*\* 0 of 1 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-invalid-var-range/test.desc

@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
 ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
-
 ^\*\* 0 of 6 failed \(1 iteration\)$
 ^\VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-not-exists/test.desc

@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] failure 1: FAILURE$
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
-
 ^\*\* 2 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-not/test.desc

@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -4,6 +4,5 @@ main.c
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
-
 ^\*\* 1 of 2 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-type/test.desc

@@ -1,10 +1,16 @@
 default: tests.log
 
 test:
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 show:
 	@for dir in *; do \

regression/goto-analyzer/Makefile

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *ptr=malloc(sizeof(int));
+  *ptr=42;
+  ptr=realloc(ptr, 20);
+  assert(*ptr==42);
+
+  int *ptr2=malloc(2*sizeof(int));
+  *ptr2=42;
+  *(ptr2+1)=42;
+  ptr2=realloc(ptr2, 20);
+  assert(*ptr2==42);
+  assert(*(ptr2+1)==42);
+
+  return 0;
+}

regression/goto-instrument/slice22/main.c

@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice22/test.desc

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+#include <assert.h>
+
+void foo(int argc)
+{
+  void* x=0;
+
+  if(argc>3)
+    x=malloc(4*sizeof(int));
+  else
+    x=malloc(3*sizeof(int));
+  *(int*)x=42;
+
+  x=realloc(x, sizeof(int));
+
+  assert(*(int*)x==42);
+}
+
+int main(int argc, char* argv[])
+{
+//__CPROVER_ASYNC_1:
+  foo(argc);
+
+  return 0;
+}

regression/goto-instrument/slice23/main.c

@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice23/test.desc

@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 ^Hello$
 --

regression/test-script/excluded-line/program.c

@@ -0,0 +1,3 @@
+Hello
+World
+

regression/test-script/excluded-line/test.desc

@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Hello$
 --

regression/test-script/excluded-line/test.txt

@@ -0,0 +1,3 @@
+Hello
+World
+

regression/test-script/failing-excluded-line/program.c

@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nAnother\nWorld

regression/test-script/failing-excluded-line/test.desc

@@ -0,0 +1,3 @@
+Hello
+World
+

regression/test-script/failing-excluded-line/test.txt

@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Goodbye$
 --

regression/test-script/failing-multi-line/program.c

@@ -0,0 +1,3 @@
+Hello
+World
+

regression/test-script/failing-multi-line/test.desc

@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nWorld

regression/test-script/failing-multi-line/test.txt

@@ -0,0 +1,3 @@
+Hello
+World
+

regression/test-script/failing-single-line/program.c

@@ -2,5 +2,4 @@
 
 set -e
 
-gcc $1 -o a.out
-./a.out
+cat $1