More tests for static and dynamic arrays

Floating point numbers cannot be extracted for now.

Author: petr-bauch

regression/snapshot-harness/arrays_02/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int array[] = {1, 2, 3};
+int *p;
+int *q;
+
+void initialize()
+{
+  p = &(array[1]);
+  q = array + 1;
+  array[0] = 4;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(p == q);
+  assert(*p == *q);
+  *p = 4;
+  q = q - 1;
+  assert(*q == *p);
+}

regression/snapshot-harness/arrays_02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion p == q: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion \*p == \*q: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion \*q == \*p: SUCCESS
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/snapshot-harness/dynamic-array-int/main.c

@@ -0,0 +1,47 @@
+#include <assert.h>
+#include <malloc.h>
+
+int *array;
+int *iterator1;
+int *iterator2;
+int *iterator3;
+
+void initialize()
+{
+  array = (int *)malloc(sizeof(int) * 10);
+  array[0] = 1;
+  array[1] = 2;
+  array[2] = 3;
+  array[3] = 4;
+  array[4] = 5;
+  array[5] = 6;
+  array[6] = 7;
+  array[7] = 8;
+  array[8] = 9;
+  array[9] = 10;
+  iterator1 = (int *)array;
+  iterator2 = &array[1];
+  iterator3 = array + 1;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 == 1);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == iterator3);
+  assert(iterator2 == &array[1]);
+  assert(*iterator3 == array[1]);
+  assert(*iterator3 == 2);
+  iterator3 = &array[9];
+  iterator3++;
+  assert(*iterator3 == 0);
+
+  return 0;
+}

regression/snapshot-harness/dynamic-array-int/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+array,iterator1,iterator2,iterator3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion \*iterator1 == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion iterator1 != iterator2: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion iterator2 == iterator3: SUCCESS
+\[main.assertion.4\] line [0-9]+ assertion iterator2 == \&array\[1\]: SUCCESS
+\[main.assertion.5\] line [0-9]+ assertion \*iterator3 == array\[1\]: SUCCESS
+\[main.assertion.6\] line [0-9]+ assertion \*iterator3 == 2: SUCCESS
+\[main.pointer_dereference.27\] line [0-9]+ dereference failure: pointer outside object bounds in \*iterator3: FAILURE
+\[main.assertion.7\] line [0-9]+ assertion \*iterator3 == 0: FAILURE
+VERIFICATION FAILED
+--
+unwinding assertion loop \d+: FAILURE

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

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+float array[10];
+float *iterator1;
+float *iterator2;
+
+void initialize()
+{
+  array[0] = 1.11;
+  array[8] = 9.999;
+  array[9] = 10.0;
+  iterator1 = (float *)array;
+  iterator2 = &array[9];
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 >= 1.10 && *iterator1 <= 1.12);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == &array[9]);
+  iterator2++;
+  assert(*iterator2 == 0.0);
+
+  return 0;
+}

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

@@ -0,0 +1,15 @@
+FUTURE
+main.c
+array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion \*iterator1 \>= 1.10 \&\& \*iterator1 \<= 1.12: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion iterator1 != iterator2: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion iterator2 == \&array\[9\]: SUCCESS
+\[main.pointer_dereference.13\] line [0-9]+ dereference failure: pointer outside object bounds in \*iterator2: FAILURE
+\[main.assertion.4\] line [0-9]+ assertion \*iterator2 == 0: FAILURE
+VERIFICATION FAILED
+--
+unwinding assertion loop \d+: FAILURE
+--
+memory analyzer does not yet allow extract floating point values

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

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+int array[10];
+int *iterator1;
+int *iterator2;
+
+void initialize()
+{
+  array[0] = 1;
+  array[8] = 9;
+  array[9] = 10;
+  iterator1 = (int *)array;
+  iterator2 = &array[9];
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 == 1);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == &array[9]);
+  iterator2++;
+  assert(*iterator2 == 0);
+
+  return 0;
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion \*iterator1 == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion iterator1 != iterator2: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion iterator2 == \&array\[9\]: SUCCESS
+\[main.pointer_dereference.13\] line [0-9]+ dereference failure: pointer outside object bounds in \*iterator2: FAILURE
+\[main.assertion.4\] line [0-9]+ assertion \*iterator2 == 0: FAILURE
+VERIFICATION FAILED
+--
+unwinding assertion loop \d+: FAILURE