Add regression tests for havoc-ing of function arguments

Author: danpoe

regression/goto-instrument/generate-function-body-havoc-params-simple-null/main.c

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

regression/goto-instrument/generate-function-body-havoc-params-simple-null/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p --pointer-check
+^SIGNAL=0$
+^EXIT=0$
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-simple/main.c

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

regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion i == 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st2 *to_st2;
+  int data;
+} st1_t;
+
+typedef struct st2
+{
+  struct st1 *to_st1;
+  int data;
+} st2_t;
+
+st1_t dummy1;
+st2_t dummy2;
+
+void func(st1_t *p);
+
+void main()
+{
+  st1_t st;
+
+  func(&st);
+
+  assert(st.to_st2 != NULL);
+  assert(st.to_st2->to_st1 != NULL);
+  assert(st.to_st2->to_st1->to_st2 == NULL);
+
+  assert(st.to_st2 != &dummy2);
+  assert(st.to_st2->to_st1 != &dummy1);
+}

regression/goto-instrument/generate-function-body-havoc-params-struct-mutual-recursion/test.desc

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

regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/main.c

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

regression/goto-instrument/generate-function-body-havoc-params-struct-non-recursive/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options havoc,params:p
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion st.data == 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/main.c

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

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion-2/test.desc

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

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/main.c

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

regression/goto-instrument/generate-function-body-havoc-params-struct-simple-recursion/test.desc

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