Add regression tests for nondet struct init

Author: danpoe

regression/cbmc/pointer-function-parameters-struct-mutual-recursion/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-struct-mutual-recursion/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-struct-non-recursive/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-struct-non-recursive/test.desc

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

regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/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-struct-simple-recursion-2/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-struct-simple-recursion-3/main.c

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

regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--function func --min-null-tree-depth 2 --max-nondet-tree-depth 10 --cover branch
+^EXIT=0$
+^SIGNAL=0$
+\[func.coverage.2\] file main.c line .* function func block 1 branch false: SATISFIED
+\[func.coverage.3\] file main.c line .* function func block 1 branch true: FAILED
+\[func.coverage.4\] file main.c line .* function func block 2 branch false: SATISFIED
+\[func.coverage.5\] file main.c line .* function func block 2 branch true: FAILED
+\[func.coverage.6\] file main.c line .* function func block 3 branch false: SATISFIED
+\[func.coverage.7\] file main.c line .* function func block 3 branch true: SATISFIED
+--
+^warning: ignoring

regression/cbmc/pointer-function-parameters-struct-simple-recursion/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-struct-simple-recursion/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

scripts/delete_failing_smt2_solver_tests

@@ -156,6 +156,11 @@ rm no_nondet_static/test.desc
 rm null1/test.desc
 rm pointer-function-parameters/test.desc
 rm pointer-function-parameters-2/test.desc
+rm pointer-function-parameters-struct-mutual-recursion/test.desc
+rm pointer-function-parameters-struct-non-recursive/test.desc
+rm pointer-function-parameters-struct-simple-recursion/test.desc
+rm pointer-function-parameters-struct-simple-recursion-2/test.desc
+rm pointer-function-parameters-struct-simple-recursion-3/test.desc
 rm scanf1/test.desc
 rm simple_assert/test.desc
 rm stack-trace/test.desc