Merge pull request #194 from theyoucheng/unwind

Unwinding operation of goto-instrument

Author: Daniel Kroening

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

regression/goto-instrument-unwind/nested-loops2/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=6;
+  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 (2): the inner one");
+
+  }
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "Nested loops unwind (2)");
+
+}

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

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

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

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

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

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