Refined test cases, on nested loops, for the unwind option of goto-instrument.

Author: theyoucheng

regression/goto-instrument-unwind/nested-loops1/:wq

@@ -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/desc

@@ -0,0 +1,7 @@
+CORE
+aclwdrr002.c
+POWER OPT
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^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/desc

@@ -0,0 +1,7 @@
+CORE
+aclwdrr002.c
+POWER OPT
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^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