Add support for void* pointers in goto-harness

regression/goto-harness/do_not_nondet_globals_by_default/main.c

@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int a_global;
 
 void entry_function(void)

regression/goto-harness/havoc-global-int-01/main.c

@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int x = 1;
 
 int main()

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

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdbool.h>
+
+void test_function(void *input)
+{
+  assert(input == 0);
+}
+
+void test_void_array(void *input_array[10])
+{
+  __CPROVER_assume(input_array != 0);
+  assert(input_array[0] == 0);
+  assert(false);
+}

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

@@ -0,0 +1,12 @@
+CORE
+main.c
+--harness-type call-function --function test_void_array
+\[test_void_array\.assertion\.1\] line \d+ assertion input_array\[0\] == 0: SUCCESS
+\[test_void_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.

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+--harness-type call-function --function test_function
+\[test_function\.assertion\.1\] line \d+ assertion input == 0: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure the harness is able to initalize a void* ptr to a null value.

src/goto-harness/recursive_initialization.cpp

@@ -621,14 +621,23 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   const typet &type = result.type().subtype();
   PRECONDITION(type.id() == ID_pointer);
 
-  code_blockt body{};
+  null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
+  const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
 
+  // always initalize void* pointers as NULL
+  if(type.subtype().id() == ID_empty)
+  {
+    return code_blockt{{assign_null, code_returnt{}}};
+  }
+
+  code_blockt body{};
   // build:
   // void type_constructor_ptr_T(int depth, T** result)
   // {
   //   if(has_seen && depth >= max_depth)
   //     *result=NULL;
-  //   else if(depth < min_null_tree_depth || nondet()) {
+  //     return
+  //   if(nondet()) {
   //     size_t has_seen_prev;
   //     has_seen_prev = T_has_seen;
   //     T_has_seen = 1;
@@ -654,11 +663,7 @@ code_blockt recursive_initializationt::build_pointer_constructor(
     should_not_recurse.push_back(has_seen_expr);
   }
 
-  null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
-  code_blockt null_and_return{};
-  code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
-  null_and_return.add(assign_null);
-  null_and_return.add(code_returnt{});
+  code_blockt null_and_return{{assign_null, code_returnt{}}};
   body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
 
   exprt::operandst should_recurse_ops{