Rewrite the recursive constructors

Previously all recursive initialisation took place in a single function. Now
each type has it's own constructor function, which are called recursively. The
results (variables to be initialised) are passed by pointer.

Author: petr-bauch

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

@@ -3,6 +3,6 @@ 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
+\[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/goto-harness/pointer-to-array-function-parameters/test.desc

@@ -1,8 +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
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/goto-harness/function_call_harness_generator.cpp

@@ -10,6 +10,7 @@ Author: Diffblue Ltd.
 
 #include <util/allocate_objects.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -53,6 +54,8 @@ struct function_call_harness_generatort::implt
   std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
   std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
 
+  std::set<symbol_exprt> global_pointers;
+
   /// \see goto_harness_generatort::generate
   void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
   /// Iterate over the symbol table and generate initialisation code for
@@ -194,6 +197,11 @@ void function_call_harness_generatort::implt::generate(
 
   generate_nondet_globals(function_body);
   call_function(arguments, function_body);
+  for(const auto &global_pointer : global_pointers)
+  {
+    function_body.add(code_function_callt{
+      recursive_initialization->get_free_function(), {global_pointer}});
+  }
   add_harness_function_to_goto_model(std::move(function_body));
 }
 
@@ -228,7 +236,10 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
   code_blockt &block,
   const exprt &lhs)
 {
-  recursive_initialization->initialize(lhs, 0, {}, block);
+  recursive_initialization->initialize(
+    lhs, from_integer(0, signed_int_type()), block);
+  if(lhs.type().id() == ID_pointer)
+    global_pointers.insert(to_symbol_expr(lhs));
 }
 
 void function_call_harness_generatort::validate_options(
@@ -366,6 +377,8 @@ void function_call_harness_generatort::implt::call_function(
   for(auto const &argument : arguments)
   {
     generate_initialisation_code_for(function_body, argument);
+    if(argument.type().id() == ID_pointer)
+      global_pointers.insert(to_symbol_expr(argument));
   }
   code_function_callt function_call{function_to_call.symbol_expr(),
                                     std::move(arguments)};

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -17,6 +17,8 @@ Author: Daniel Poetzl
 
 #include <json-symtab-language/json_symbol_table.h>
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/fresh_symbol.h>
 #include <util/message.h>
@@ -290,7 +292,9 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
     else
     {
       recursive_initialization.initialize(
-        fresh_or_snapshot_symbol.symbol_expr(), 0, {}, code);
+        fresh_or_snapshot_symbol.symbol_expr(),
+        from_integer(0, size_type()),
+        code);
     }
   }
   return code;