Add a test for the new preorder linearisation

when setting the order in which to initialise the variables from a snapshot.
This test is designed to be failing slightly more often than the
`dynamic-array-int` test by inserting extra variables in between the
preordered ones. They cannot be named `array` because that irep-name already
exists.

Author: petr-bauch

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

@@ -0,0 +1,64 @@
+#include <assert.h>
+#include <malloc.h>
+
+int a;
+int *a1;
+int *iterator1;
+int *a2;
+int *a3;
+int *iterator2;
+int *a4;
+int *a5;
+int *iterator3;
+int *a6;
+int *a7;
+int *array2;
+int *a8;
+
+void initialize()
+{
+  array2 = (int *)malloc(sizeof(int) * 10);
+  array2[0] = 1;
+  array2[1] = 2;
+  array2[2] = 3;
+  array2[3] = 4;
+  array2[4] = 5;
+  array2[5] = 6;
+  array2[6] = 7;
+  array2[7] = 8;
+  array2[8] = 9;
+  array2[9] = 10;
+  iterator1 = (int *)array2;
+  iterator2 = &array2[1];
+  iterator3 = array2 + 1;
+  a1 = &a;
+  a2 = a1;
+  a3 = a2;
+  a4 = a3;
+  a5 = a4;
+  a6 = a5;
+  a7 = a6;
+  a8 = a7;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 == 1);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == iterator3);
+  assert(iterator2 == &array2[1]);
+  assert(*iterator3 == array2[1]);
+  assert(*iterator3 == 2);
+  iterator3 = &array2[9];
+  iterator3++;
+  assert(*iterator3 == 0);
+
+  return 0;
+}

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

@@ -0,0 +1,16 @@
+CORE
+main.c
+a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --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 == \&array2\[1\]: SUCCESS
+\[main.assertion.5\] line [0-9]+ assertion \*iterator3 == array2\[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