Add a test for an array we can initalize

Here the array contains pointers, so we can sensibly create a non-null
array here.

Author: Thomas Kiley

regression/goto-harness/void-star-pointer/main.c

@@ -12,3 +12,10 @@ void test_void_array(void *input_array[10])
   assert(input_array[0] == 0);
   assert(false);
 }
+
+void test_ptr_array(void **input_array)
+{
+  __CPROVER_assume(input_array != 0);
+  assert(input_array[0] == 0);
+  assert(false);
+}

regression/goto-harness/void-star-pointer/test-array-as-array.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--harness-type call-function --function test_ptr_array --treat-pointer-as-array input_array
+\[test_ptr_array\.assertion\.1\] line \d+ assertion input_array\[0\] == 0: SUCCESS
+\[test_ptr_array\.assertion\.2\] line \d+ assertion false: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Ensure the harness is able to initalize an array of void* pointers where
+the array is non-null, but the elements are null, if the void** is treated as an
+array.