Regression tests for user-control havoc

Char-arrays don't work for now. Structs and non-char pointers do.

Author: Petr Bauch

regression/snapshot-harness/nondet_initialize_static_arrays/main.c

@@ -0,0 +1,51 @@
+#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;
+
+typedef struct st3
+{
+  st1_t *array[3];
+} st3_t;
+
+st3_t *p;
+
+void initialize()
+{
+  p = malloc(sizeof(st3_t));
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(p != NULL);
+  for(int index = 0; index < 3; index++)
+  {
+    // check that the arrays in structs (and structs in those arrays) were
+    // initialized up-to the input depth
+    assert(p->array[index]->to_st2 != NULL);
+    assert(p->array[index]->to_st2->to_st1 != NULL);
+    assert(p->array[index]->to_st2->to_st1->to_st2 == NULL);
+  }
+
+  // non-deterministically initializated objects should not be equal
+  assert(p->array[0] != p->array[1]);
+  assert(p->array[1] != p->array[2]);
+  assert(p->array[0] != p->array[2]);
+}

regression/snapshot-harness/nondet_initialize_static_arrays/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+p --harness-type initialise-with-memory-snapshot --initial-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/main.c

@@ -0,0 +1,42 @@
+#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;
+
+st1_t *p;
+
+void initialize()
+{
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  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/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+p --harness-type initialise-with-memory-snapshot --initial-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer-to-array-char/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+#include <malloc.h>
+
+char *first;
+char *second;
+int array_size;
+
+void initialize()
+{
+  first = malloc(sizeof(char) * 12);
+  first = "1234567890a";
+  second = first;
+  array_size = 11;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  assert(second[array_size - 1] == 'a');
+  //  assert(second[10]=='0');
+  return 0;
+}

regression/snapshot-harness/pointer-to-array-char/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+first,second,array_size --harness-type initialise-with-memory-snapshot --initial-location main:4
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+
+char *first = "12345678901";
+char *second;
+int string_size;
+const char *prefix;
+int prefix_size;
+
+void initialize()
+{
+  second = first;
+  string_size = 11;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  if(prefix_size > 0)
+    assert(second[prefix_size - 1] != 'a');
+
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+
+  for(int ix = 0; ix < prefix_size; ++ix)
+  {
+    if(second[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-location main:4 --havoc-variables prefix,prefix_size --size-of-array prefix:prefix_size --max-array-size 5
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer-to-array-int/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <malloc.h>
+
+int *first;
+int *second;
+int array_size;
+const int *prefix;
+int prefix_size;
+
+void initialize()
+{
+  first = malloc(sizeof(int) * 5);
+  second = first;
+  array_size = 5;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  assert(array_size >= prefix_size);
+  assert(prefix_size >= 0);
+  assert(second[prefix_size] != 6);
+
+  for(int i = 0; i < prefix_size; i++)
+    assert(second[i] != prefix[i]);
+  return 0;
+}

regression/snapshot-harness/pointer-to-array-int/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+temp,first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/static-array-char/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+char tmp[12];
+char *first;
+char *second;
+int array_size;
+
+void initialize()
+{
+  tmp[0] = '1';
+  tmp[9] = '0';
+  tmp[10] = 'a';
+  first = (char *)tmp;
+  second = first;
+  array_size = 11;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  assert(second[array_size - 1] == 'a');
+  assert(first[0] == '1');
+  assert(second[9] == '0');
+  return 0;
+}

regression/snapshot-harness/static-array-char/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-location main:4
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE