Incremental unwinding of one specified loop

regression/cbmc-incr-oneloop/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "perl -e 'alarm shift @ARGV; exec @ARGV' 8 $<TARGET_FILE:cbmc> --slice-formula"
+)

regression/cbmc-incr-oneloop/Makefile

@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
 
 show:
 	@for dir in *; do \

regression/cbmc-incr-oneloop/alarm1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 25 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-max 15
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/alarm2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-min 5 --unwind-max 10 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-min 5 --unwind-max 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/alarm3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0
+--incremental-loop main.0 --unwind-max 15 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/arrays2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 5  --no-unwinding-assertions --arrays-uf-always
+--incremental-loop main.0 --unwind-max 5 --arrays-uf-always
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/arrays3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --no-unwinding-assertions --arrays-uf-always
+--incremental-loop main.0 --arrays-uf-always
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/arrays4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --no-unwinding-assertions --arrays-uf-always
+--incremental-loop main.0 --arrays-uf-always
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/arrays5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 5 --no-unwinding-assertions --arrays-uf-always
+--incremental-loop main.0 --unwind-max 5 --arrays-uf-always
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/assertion-after-loop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-loop main.0
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/assertion-after-loop2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-loop main.0
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/cruise1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 10 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-max 10
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/cruise2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0
+--incremental-loop main.0 --unwind-max 10 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/induction1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --stop-when-unsat --no-unwinding-assertions
+--incremental-loop main.0 --stop-when-unsat
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/induction2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --stop-when-unsat --no-unwinding-assertions
+--incremental-loop main.0 --stop-when-unsat
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/minmaxunwind1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-min 4 --unwind-max 6 --incremental-check main.0
+--unwind-min 4 --unwind-max 6 --incremental-loop main.0
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/minmaxunwind2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-min 5 --unwind-max 5 --incremental-check main.0
+--unwind-min 5 --unwind-max 5 --incremental-loop main.0
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/minmaxunwind3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-min 2 --unwind-max 4 --incremental-check main.0
+--unwind-min 2 --unwind-max 4 --incremental-loop main.0
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/minmaxunwind4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-min 6 --unwind-max 8 --incremental-check main.0
+--unwind-min 6 --unwind-max 8 --incremental-loop main.0
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/minmaxunwind5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-min 4 --unwind-max 6 --incremental-check main.1
+--unwind-min 4 --unwind-max 6 --incremental-loop main.1
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/moreasserts1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0
+--incremental-loop main.0 --unwinding-assertions --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/nestedloop1/main.c

@@ -3,9 +3,9 @@ int main()
 {
   int x = nondet_int();
   __CPROVER_assume(0<=x && x<=1);
-  while(x<4) {
+  while(x<4) { // main.1
     int y = 5;
-    while(y>2) y-=2;
+    while(y>2) y-=2; // main.0
     x=x+y;
     assert(x<4);
   }

regression/cbmc-incr-oneloop/nestedloop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0
+--incremental-loop main.1 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-loop main.0
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/simpleloop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0
+--incremental-loop main.0 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/simpleloop2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 6 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-max 6
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/simpleloop3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0  --no-unwinding-assertions
+--incremental-loop main.0
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/simpleloopmax1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-loop main.0
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/simpleloopmax2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-unwinding-assertions --unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-loop main.0
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/simplifier1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 5 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-max 5
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/simplifier2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 3 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-max 3 --stop-on-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/simplifier3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---incremental-check main.0 --unwind-max 5 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-max 5
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-incr-oneloop/unwind-forever1/main.c

@@ -3,9 +3,9 @@ int main()
 {
   int x = nondet_int();
   __CPROVER_assume(0<=x && x<=1);
-  //no error within loop => will unwind forever if no loop bound is given
+  // no error within loop => will unwind forever if no loop bound is given
   while(x<4) {
     x=x+1;
   }
-  assert(x<4);
+  assert(x < 4); // goto-symex never gets here unless it detects the loop bound
 }

regression/cbmc-incr-oneloop/unwind-forever1/test.desc

@@ -1,7 +1,10 @@
-CORE
+THOROUGH
 main.c
- --incremental-check main.0
-^EXIT=142$
+--incremental-loop main.0 --unwinding-assertions
+^EXIT=(142|14)$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+Tests whether goto-symex does not stop early.
+Mac OS exit code is 14

regression/cbmc-incr-oneloop/unwind-forever2/main.c

@@ -3,9 +3,10 @@ int main()
 {
   int x = nondet_int();
   __CPROVER_assume(0<=x && x<=1);
-  //no error within loop => will unwind forever if no loop bound is given
+  // no error within loop => will unwind forever if no loop bound is given
   while(x<4) {
     x=x+1;
     assert(x<=4);
   }
+  assert(x < 4); // goto-symex never gets here unless it detects the loop bound
 }

regression/cbmc-incr-oneloop/unwind-forever2/test.desc

@@ -1,7 +1,11 @@
-CORE
+THOROUGH
 main.c
---incremental-check main.0
-^EXIT=142$
+--incremental-loop main.0 --unwinding-assertions
+^EXIT=(142|14)$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+Tests whether goto-symex does not stop early when it cannot figure out the
+loop bound and there is no error in the loop.
+Mac OS exit code is 14

regression/cbmc-incr-oneloop/unwind-more-loops1/main.c

@@ -0,0 +1,16 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 1);
+  while(1) // main.0
+  {
+    if(nondet_int())
+      break;
+  }
+  while(x < 4) // main.1
+  {
+    x = x + 1;
+    assert(x < 4);
+  }
+}

regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--incremental-loop main.1 --unwind 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^Not unwinding loop main\.0 iteration 2
+^Unwinding loop main\.1 iteration 3
+--
+^warning: ignoring
+--

regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-loop main.0 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/unwindset-more-loops1/main.c

@@ -0,0 +1,28 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 1);
+  int y = 0;
+  while(y < 5) // main.0
+  {
+    y++;
+    if(nondet_int())
+      break;
+  }
+  while(1) // main.1
+  {
+    if(nondet_int())
+      break;
+  }
+  while(x < 4) // main.3
+  {
+    while(1) // main.2
+    {
+      if(nondet_int())
+        break;
+    }
+    x = x + 1;
+    assert(x < 4);
+  }
+}

regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--incremental-loop main.3 --unwindset main.1:2,main.2:8
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^Unwinding loop main\.0 iteration 5
+^Not unwinding loop main\.1 iteration 2
+^Not unwinding loop main\.2 iteration 8
+^Unwinding loop main\.3 iteration 3
+--
+^warning: ignoring
+^Unwinding loop main\.0 iteration 6