Merge pull request #4181 from NlightNFotis/non-det-struct-new

Non-deterministic initialisation of structs, pointers and globals in function call harness

Author: NlightNFotis

regression/goto-harness/do_not_nondet_globals_by_default/main.c

@@ -0,0 +1,6 @@
+int a_global;
+
+void entry_function(void)
+{
+  assert(a_global == 0);
+}

regression/goto-harness/do_not_nondet_globals_by_default/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function entry_function
+^\[entry_function.assertion.1\] line \d+ assertion a_global == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/goto-harness/non_det_globals_option/main.c

@@ -0,0 +1,6 @@
+int a_global;
+
+void entry_function(void)
+{
+  assert(a_global == 0);
+}

regression/goto-harness/non_det_globals_option/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function entry_function --nondet-globals
+^\[entry_function.assertion.1\] line \d+ assertion a_global == 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

regression/goto-harness/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/goto-harness/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 --harness-type call-function
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/goto-harness/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/goto-harness/pointer-function-parameters-struct-non-recursive/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --harness-type call-function
+^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/goto-harness/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/goto-harness/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  --harness-type call-function
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/goto-harness/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/goto-harness/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 --harness-type call-function
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct A A;
+typedef struct B B;
+typedef struct C C;
+typedef struct D D;
+
+struct A
+{
+  B *b;
+};
+
+struct B
+{
+  C *c;
+};
+
+struct C
+{
+  D *d;
+};
+
+struct D
+{
+  A *a;
+};
+
+void func(A *a)
+{
+  assert(a != NULL);
+  assert(a->b != NULL);
+  assert(a->b->c != NULL);
+  assert(a->b->c->d != NULL);
+  assert(a->b->c->d->a == NULL);
+}

regression/goto-harness/recursive-structs-follow-new-tags-beyond-depth-limit/test.desc

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

src/goto-harness/Makefile

@@ -4,6 +4,7 @@ SRC = \
   goto_harness_generator_factory.cpp \
   goto_harness_main.cpp \
   goto_harness_parse_options.cpp \
+  recursive_initialization.cpp \
   # Empty last line
 
 OBJ += \