Remove dead method from recursive initialization

The ::build_array_string_constructor method was originally intended to be used
for building C string constructors. Unfortunately as written the condition for
calling it was actually impossible to satisfy. This wasn’t noticed so far
because similar code is now generated in ::build_dynamic_array_constructor
instead.

Dead code is a maintenance burden so it’s removed here.

Author: hannes-steffenhagen-diffblue

src/goto-harness/recursive_initialization.cpp

@@ -265,9 +265,7 @@ code_blockt recursive_initializationt::build_constructor_body(
     }
     if(lhs_name.has_value())
     {
-      if(should_be_treated_as_cstring(*lhs_name) && type == char_type())
-        return build_array_string_constructor(result_symbol);
-      else if(should_be_treated_as_array(*lhs_name))
+      if(should_be_treated_as_array(*lhs_name))
       {
         CHECK_RETURN(size_symbol.has_value());
         return build_dynamic_array_constructor(
@@ -740,36 +738,6 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   return body;
 }
 
-code_blockt recursive_initializationt::build_array_string_constructor(
-  const symbol_exprt &result) const
-{
-  PRECONDITION(result.type().id() == ID_pointer);
-  const typet &type = result.type().subtype();
-  PRECONDITION(type.id() == ID_array);
-  PRECONDITION(type.subtype() == char_type());
-  const array_typet &array_type = to_array_type(type);
-  const auto array_size =
-    numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
-  code_blockt body{};
-
-  for(std::size_t index = 0; index < array_size - 1; index++)
-  {
-    index_exprt index_expr{dereference_exprt{result},
-                           from_integer(index, size_type())};
-    auto const nondet_char =
-      get_fresh_local_typed_symexpr("nondet_char", char_type());
-    body.add(code_declt{nondet_char});
-    body.add(code_assignt{index_expr, nondet_char});
-    body.add(code_assumet{
-      notequal_exprt{index_expr, from_integer(0, array_type.subtype())}});
-  }
-  body.add(code_assignt{index_exprt{dereference_exprt{result},
-                                    from_integer(array_size - 1, size_type())},
-                        from_integer(0, array_type.subtype())});
-
-  return body;
-}
-
 code_blockt recursive_initializationt::build_array_constructor(
   const exprt &depth,
   const symbol_exprt &result)

src/goto-harness/recursive_initialization.h

@@ -262,11 +262,6 @@ class recursive_initializationt
     const exprt &size,
     const optionalt<irep_idt> &lhs_name);
 
-  /// Constructor for strings: as array but the last element is zero.
-  /// \param result: symbol of the result parameter
-  /// \return the body of the constructor
-  code_blockt build_array_string_constructor(const symbol_exprt &result) const;
-
   /// Select the specified struct-member to be non-deterministically
   ///   initialized.
   /// \param lhs: symbol expression of the top structure