goto instrument loop unwinding with strategies

Author: danpoe

regression/Makefile

@@ -1,4 +1,4 @@
-DIRS = ansi-c cbmc cpp goto-instrument
+DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)

regression/goto-instrument-unwind/Makefile

@@ -21,9 +21,10 @@ tests.log: ../test.pl
 clean:
 	@for dir in *; do \
                 if [ -d "$$dir" ]; then \
-                        rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
+                        rm -f $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
                 fi; \
-        done;
+  done;
+	rm -f tests.log
 
 show:
 	@for dir in *; do \

regression/goto-instrument-unwind/assert1/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/assert1/test.desc

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

regression/goto-instrument-unwind/assert2/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/assert2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 9 --unwinding-assertions
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assert3/main.c

@@ -0,0 +1,9 @@
+
+int main()
+{
+  int i;
+  i = 0;
+  do {
+    i++;
+  } while(i < 10);
+}

regression/goto-instrument-unwind/assert3/test.desc

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

regression/goto-instrument-unwind/assume1/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+  assert(0);
+}

regression/goto-instrument-unwind/assume1/test.desc

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