Implement initialization of dynamic array parameters

This implements the behaviour of the

--pointers-to-treat-as-arrays
--associated-array-sizes
--max-dynamic-array-size

options.

Author: hannes-steffenhagen-diffblue

regression/cbmc/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/cbmc/pointer-to-array-function-parameters-max-size/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --max-dynamic-array-size 20 --pointer-check --unwind 20 --associated-array-sizes arr:sz
+\[test.assertion.1\] line \d+ assertion sz <= 10: FAILURE
+\[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
+EXIT=10
+SIGNAL=0

regression/cbmc/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/cbmc/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -0,0 +1,6 @@
+CORE
+test.c
+--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 20
+SIGNAL=0
+EXIT=0
+VERIFICATION SUCCESSFUL

regression/cbmc/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/cbmc/pointer-to-array-function-parameters-multi-arg-wrong/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.c
+--function is_prefix_of --pointers-to-treat-as-arrays string,prefix --associated-array-sizes string:string_size,prefix:prefix_size --pointer-check --unwind 10
+EXIT=10
+SIGNAL=0
+\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
+VERIFICATION FAILED

regression/cbmc/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/cbmc/pointer-to-array-function-parameters-with-size/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 10 --associated-array-sizes 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/cbmc/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/cbmc/pointer-to-array-function-parameters/test.desc

@@ -0,0 +1,6 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-arrays arr --pointer-check --unwind 20
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.12\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
+--