Merge pull request #165 from diffblue/feature/wrap_entry_point

[TYT-2] Support for wrapping the entry point in an infinite loop in the different tools

Author: NlightNFotis

regression/cbmc/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/cbmc/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=0$
+^SIGNAL=0$
+^     1: main\(argc', argv'\);$
+^        GOTO 1$
+--

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -0,0 +1,4 @@
+int skipWhitespace()
+{
+    return 120;
+}

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
+^EXIT=0$
+^SIGNAL=0$
+^     1: skipWhitespace\(\);$
+^        GOTO 1$
+--

regression/goto-analyzer/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/goto-analyzer/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=6$
+^SIGNAL=0$
+^     1: IF FALSE THEN GOTO 2$
+^        main\(argc', argv'\);$
+^        GOTO 1$
+--

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -0,0 +1,4 @@
+int skipWhitespace()
+{
+    return 120;
+}

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
+^EXIT=6$
+^SIGNAL=0$
+^     1: IF FALSE THEN GOTO 2$
+^        skipWhitespace\(\);$
+^        GOTO 1$
+--

regression/goto-instrument/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/goto-instrument/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=0$
+^SIGNAL=0$
+^     1: main\(argc', argv'\);$
+^        GOTO 1$
+--
+--
+This is tracked by the JIRA issue TYT-4: https://diffblue.atlassian.net/projects/TYT/issues/TYT-4