Merge pull request #5408 from thomasspriggs/tas/fix-array-types

Fix type mismatch in goto-harness on calling array constructor.

Author: Thomas Kiley

regression/goto-harness/array-types/example.c

@@ -0,0 +1,4 @@
+void test(signed int *arr)
+{
+  arr[0l] = 5;
+}

regression/goto-harness/array-types/test.desc

@@ -0,0 +1,11 @@
+CORE
+example.c
+--harness-type call-function --function test --treat-pointer-as-array arr
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+type_constructor_ptr_int\(0, &arr, \(signed int \*\)\(void \*\)0\);
+--
+incompatible pointer types
+--
+Ensure that the function pointer types match

src/goto-harness/recursive_initialization.cpp

@@ -209,12 +209,12 @@ void recursive_initializationt::initialize(
       {
         const auto &fun_type_params =
           to_code_type(fun_symbol.type).parameters();
-        const typet &size_var_type = fun_type_params.back().type();
+        const pointer_typet *size_var_type =
+          type_try_dynamic_cast<pointer_typet>(fun_type_params.back().type());
+        INVARIANT(size_var_type, "Size parameter must have pointer type.");
         body.add(code_function_callt{
           fun_symbol.symbol_expr(),
-          {depth,
-           address_of_exprt{lhs},
-           null_pointer_exprt{pointer_type(size_var_type)}}});
+          {depth, address_of_exprt{lhs}, null_pointer_exprt{*size_var_type}}});
       }
       return;
     }