Add array initialisation support in default goto-harness.

regression/goto-harness/associated-size-parameter/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+void test(int *array, int size)
+{
+  for(int i = 0; i < size; i++)
+    array[i] = i;
+
+  for(int i = 0; i < size; i++)
+    assert(array[i] == i);
+}

regression/goto-harness/associated-size-parameter/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function test --associated-array-size array:size
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-harness/chain.sh

@@ -23,5 +23,11 @@ if [ -e "${name}-mod.gb" ] ; then
   rm -f "${name}-mod.gb"
 fi
 
-$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} 
-$cbmc --function $entry_point "${name}-mod.gb" --unwind 20 --unwinding-assertions
+# `# some comment` is an inline comment - basically, cause bash to execute an empty command
+
+$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
+$cbmc --function $entry_point "${name}-mod.gb" \
+  --pointer-check `# because we want to see out of bounds errors` \
+  --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
+  --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
+  # cbmc args end

regression/goto-harness/nondet_initialize_static_arrays/main.c

@@ -0,0 +1,37 @@
+#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;
+
+st1_t dummy1;
+st2_t dummy2;
+
+void func(st3_t *p)
+{
+  assert(p != NULL);
+  for(int index = 0; index < 3; index++)
+  {
+    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);
+  }
+
+  assert(p->array[0] != p->array[1]);
+  assert(p->array[1] != p->array[2]);
+  assert(p->array[0] != p->array[2]);
+}

regression/goto-harness/nondet_initialize_static_arrays/test.desc

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

regression/goto-harness/pointer-to-array-function-parameters-max-size/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+void test(int *arr, int sz)
+{
+  assert(sz < 10);
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}

regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc

@@ -0,0 +1,14 @@
+CORE
+test.c
+--harness-type call-function --function test --max-array-size 10 --associated-array-size arr:sz
+\[test.assertion.1\] line \d+ assertion sz < 10: FAILURE
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+unwinding assertion loop \d: FAILURE

regression/goto-harness/pointer-to-array-function-parameters-min-size/test.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+void min_array_size_test(int *arr, int sz)
+{
+  assert(sz > 2);
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = i;
+  }
+  for(int i = 0; i < sz; ++i)
+  {
+    assert(arr[i] == i);
+  }
+}

regression/goto-harness/pointer-to-array-function-parameters-min-size/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function min_array_size_test --max-array-size 3 --min-array-size 3 --associated-array-size arr:sz
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+unwinding assertion loop \d: FAILURE

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-right/test.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int is_prefix_of(
+  const char *string,
+  int string_size,
+  const char *prefix,
+  int prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+
+  for(int ix = 0; ix < prefix_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

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

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stddef.h>
+
+int is_prefix_of(
+  const char *string,
+  size_t string_size,
+  const char *prefix,
+  size_t prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+  assert(prefix_size <= string_size);
+  // oh no! we should have used prefix_size here
+  for(int ix = 0; ix < string_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
+^EXIT=10$
+^SIGNAL=0$
+\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
+VERIFICATION FAILED
+--

regression/goto-harness/pointer-to-array-function-parameters-with-size/test.c

@@ -0,0 +1,7 @@
+void test(int *arr, int sz)
+{
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}

regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
+^EXIT=0$
+^SIGNAL=0$
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+--

regression/goto-harness/pointer-to-array-function-parameters/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+void test(int *arr)
+{
+  // works because the arrays we generate have at least one element
+  arr[0] = 5;
+
+  // doesn't work because our arrays have at most ten elements
+  arr[10] = 10;
+}

regression/goto-harness/pointer-to-array-function-parameters/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function test --treat-pointer-as-array arr
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--