Finished modifying the tests.

Author: NlightNFotis

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -1,4 +1,7 @@
-int skipWhitespace()
+int g = 0;
+
+int skipWhitespace(void)
 {
-    return 120;
+    assert(g == 0);
+    g = (g == 0) ? 1 : 0;
 }

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
---show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
-^EXIT=0$
+--wrap-entry-point-in-while --unwind 100 --function skipWhitespace
+^EXIT=10$
 ^SIGNAL=0$
-^     1: skipWhitespace\(\);$
-^        GOTO 1$
+^\[skipWhitespace.assertion.1\] assertion g == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+^VERIFICATION SUCCESSFUL$
 --

regression/goto-analyzer/wrap_entry_point_in_while_true/main.c

@@ -1,4 +1,7 @@
-int main(int argc, char **argv)
+int g = 0;
+
+int main(void)
 {
-    return 0;
+    assert(g == 0);
+    g = (g == 0) ? 1 : 0;
 }

regression/goto-analyzer/wrap_entry_point_in_while_true/test.desc

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

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -1,4 +1,7 @@
-int skipWhitespace()
+int g = 0;
+
+int skipWhitespace(void)
 {
-    return 120;
+    assert(g == 0);
+    g = (g == 0) ? 1 : 0;
 }