Add regression tests for nondet struct init

Author: danpoe

regression/cbmc/pointer-function-parameters-3/main.c

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

regression/cbmc/pointer-function-parameters-3/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10
+^SIGNAL=0$
+\[func.assertion.1\] assertion p != .*((NULL)|0).*: SUCCESS
+\[func.assertion.2\] assertion p != &dummy: SUCCESS
+\[func.assertion.3\] assertion p->data >= 4854549: FAILURE
+\[func.assertion.4\] assertion p->data < 4854549: FAILURE
+--
+^warning: ignoring

regression/cbmc/pointer-function-parameters-4/main.c

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

regression/cbmc/pointer-function-parameters-4/test.desc

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

regression/cbmc/pointer-function-parameters-5/main.c

@@ -0,0 +1,28 @@
+#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)
+{
+  assert(p != NULL);
+  assert(p != &dummy);
+
+  assert(p->prev != NULL);
+  assert(p->prev != &dummy);
+
+  assert(p->next != NULL);
+  assert(p->next != &dummy);
+
+  assert(p->prev->prev == NULL);
+  assert(p->prev->next == NULL);
+  assert(p->next->prev == NULL);
+  assert(p->next->next == NULL);
+}

regression/cbmc/pointer-function-parameters-5/test.desc

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

regression/cbmc/pointer-function-parameters-6/main.c

@@ -0,0 +1,29 @@
+#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)
+{
+  assert(p != NULL);
+  assert(p->to_st2 != NULL);
+  assert(p->to_st2->to_st1 != NULL);
+  assert(p->to_st2->to_st1->to_st2 == NULL);
+
+  assert(p != &dummy1);
+  assert(p->to_st2 != &dummy2);
+  assert(p->to_st2->to_st1 != &dummy1);
+}

regression/cbmc/pointer-function-parameters-6/test.desc

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