Merge remote-tracking branch 'refs/remotes/diffblue/master'

Author: AnnaTrost

.gitattributes

@@ -0,0 +1,9 @@
+*.cpp text
+*.c text
+*.h text
+*.y text
+*.tex text
+*.shtml text
+*.html text
+*.css text
+Makefile text

regression/ansi-c/array_initialization2/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int a[(int)(10./1.)];
+int b[(int)2] = { 10, 20 };
+int c[(int)(10./1.)] = { 10, 20 };
+int d[(int)(10/1)] = { 10, 20 };
+
+int main (void) {
+  if (a[0]) {
+    assert(b[1] + c[2] > 20);
+  }
+
+  return 1;
+}
+
+extern int g_array[];
+int array[(int)(10./1)];
+
+int array2[(int)(10./1)];

regression/ansi-c/array_initialization2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/Pointer_array5/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Pointer_array6/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+#include <stdlib.h>
+
+extern int nondet_int();
+
+int main() {
+
+  int arraylen=nondet_int();
+
+  if(arraylen==3)
+  {
+    int** array_init = malloc(sizeof(int *)*arraylen);
+
+    // mis-align that pointer!
+    char * char_ptr = (char *) array_init;
+    char_ptr++;
+    
+    int local_var;
+
+    int **array2=(int**)char_ptr;
+    
+    // write
+    array2[0]=&local_var;
+    
+    // check
+    int value=*array2[0];
+
+    assert(value==local_var);
+  }
+
+}

regression/cbmc/Pointer_array6/test.desc

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

regression/cbmc/big-endian-array1/main.c

@@ -7,7 +7,8 @@ int main()
   unsigned size;
   __CPROVER_assume(size==1);
 
-  array=malloc(size*sizeof(int)); // produce unbounded array
+  // produce unbounded array that does not have byte granularity
+  array=malloc(size*sizeof(int));
   array[0]=0x01020304;
 
   int array0=array[0];

regression/goto-instrument-unwind/Makefile

@@ -0,0 +1,33 @@
+default: tests.log
+
+testalpha:
+	@../test.pl -c ../unwind-chain.sh -C
+
+testbeta:
+	@../test.pl -c ../unwind-chain.sh -T
+
+testimpr:
+	@../test.pl -c ../unwind-chain.sh -K
+
+testnew:
+	@../test.pl -c ../unwind-chain.sh -F
+
+test:
+	@../test.pl -c ../unwind-chain.sh 
+
+tests.log: ../test.pl
+	@../test.pl -c ../unwind-chain.sh 
+
+clean:
+	@for dir in *; do \
+                if [ -d "$$dir" ]; then \
+                        rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
+                fi; \
+        done;
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/goto-instrument-unwind/break-loop1/main.c

@@ -0,0 +1,30 @@
+
+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;
+  unsigned tres=K/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+    if(i==tres)
+      break;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "break a loop unwind (1)");
+
+}

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

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

regression/goto-instrument-unwind/break-loop2/main.c

@@ -0,0 +1,30 @@
+
+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;
+  unsigned tres=K/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+    if(i==tres)
+      break;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "break a loop unwind (2)");
+
+}

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

@@ -0,0 +1,7 @@
+CORE
+main.c
+100
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/continue-loop1/main.c

@@ -0,0 +1,30 @@
+
+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;
+  unsigned tres=K/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    if(i>tres)
+      continue;
+    c++;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "continue in a loop unwind (1)");
+
+}

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

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

regression/goto-instrument-unwind/continue-loop2/main.c

@@ -0,0 +1,30 @@
+
+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;
+  unsigned tres=n/2;;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    if(i>tres)
+      continue;
+    c++;
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  if(tres<eva) eva=tres;
+  
+  __CPROVER_assert(c==eva, "continue in a loop unwind (2)");
+
+}

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

@@ -0,0 +1,7 @@
+CORE
+main.c
+100
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/empty-loop1/main.c

@@ -0,0 +1,22 @@
+
+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 i=0;
+
+  while(++i<n)
+  {
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(i==eva, "Empty loop unwind (1)");
+
+}

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

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

regression/goto-instrument-unwind/empty-loop2/main.c

@@ -0,0 +1,22 @@
+
+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 i=0;
+
+  while(++i<n)
+  {
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(i==eva, "Empty loop unwind (1)");
+
+}

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

@@ -0,0 +1,7 @@
+CORE
+main.c
+100
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/nested-loops1/main.c

@@ -0,0 +1,40 @@
+
+void f() {}
+void f2() {}
+
+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;
+
+  for(i=1; i<=n; i++)
+  {
+    f();
+    c++;
+
+    // the nested loop
+    unsigned j, c2=0;
+    for(j=1; j<=i; j++)
+    {
+      f2();
+      c2++;
+    }
+    unsigned eva2=i;
+    if(K<eva2) eva2=K;
+    
+    __CPROVER_assert(c2==eva2, "Nested loops unwind (1): the inner one");
+
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "Nested loops unwind (1)");
+
+}

regression/goto-instrument-unwind/nested-loops1/test.desc

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