Add regression tests for nondet return value generation

Author: danpoe

regression/goto-instrument/generate-function-body-nondet-return-const/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+const int func();
+
+void main()
+{
+  assert(func() == 0);
+  assert(func() != 0);
+}

regression/goto-instrument/generate-function-body-nondet-return-const/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion func\(\) == 0: FAILURE
+\[main.assertion.2\] line \d+ assertion func\(\) != 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-nondet-return-double-pointer/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int **func();
+
+void main()
+{
+  int **p = func();
+
+  assert(p != NULL);
+  assert(*p != NULL);
+
+  assert(**p == 0);
+  assert(**p != 0);
+}

regression/goto-instrument/generate-function-body-nondet-return-double-pointer/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return --min-null-tree-depth 10 --max-nondet-tree-depth 5
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion p != .*(0|(NULL))\)?: SUCCESS
+\[main.assertion.2\] line \d+ assertion \*p != .*(0|(NULL))\)?: SUCCESS
+\[main.assertion.3\] line \d+ assertion \*\*p == 0: FAILURE
+\[main.assertion.4\] line \d+ assertion \*\*p != 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-nondet-return-simple/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int func();
+
+void main()
+{
+  assert(func() == 0);
+  assert(func() != 0);
+}

regression/goto-instrument/generate-function-body-nondet-return-simple/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion func\(\) == 0: FAILURE
+\[main.assertion.2\] line \d+ assertion func\(\) != 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+st_t dummy;
+
+st_t *func();
+
+void main()
+{
+  st_t *st = func();
+
+  assert(st != NULL);
+
+  assert(st->next != NULL);
+  assert(st->next->next != NULL);
+  assert(st->next->next->next == NULL);
+
+  assert(st != &dummy);
+  assert(st->next != &dummy);
+  assert(st->next->next != &dummy);
+}

regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return --min-null-tree-depth 10 --max-nondet-tree-depth 3
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring