Add code for String constructor from array

The function what was there before was not correct.
It was calling cprover_string_copy which is deprecated.

Author: romainbrenguier

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1678,6 +1678,59 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
   return code;
 }
 
+/// Used to provide code for constructor from a char array.
+/// The implementation is similar to substring except the 3rd argument is a
+/// count instead of end index
+/// \param type: type of the function call
+/// \param loc: location in the program_invocation_name
+/// \param symbol_table: symbol table
+/// \return code implementing String intitialization from a char array and
+///         arguments offset and end.
+codet java_string_library_preprocesst::make_init_from_array_code(
+  const code_typet &type,
+  const source_locationt &loc,
+  symbol_tablet &symbol_table)
+{
+  // Code for the output
+  code_blockt code;
+
+  code_typet::parameterst params = type.parameters();
+  PRECONDITION(params.size() == 4);
+  exprt::operandst args =
+    process_parameters(type.parameters(), loc, symbol_table, code);
+  INVARIANT(
+    args.size() == 4, "process_parameters preserves number of arguments");
+
+  /// \todo this assumes the array to be constant between all calls to
+  /// string primitives, which may not be true in general.
+  refined_string_exprt string_arg = to_string_expr(args[1]);
+  add_pointer_to_array_association(
+    string_arg.content(),
+    dereference_exprt(
+      string_arg.content(),
+      array_typet(java_char_type(), infinity_exprt(java_int_type()))),
+    symbol_table,
+    loc,
+    code);
+
+  // The third argument is `count`, whereas the third argument of substring
+  // is `end` which corresponds to `offset+count`
+  refined_string_exprt string_expr = string_expr_of_function(
+    ID_cprover_string_substring_func,
+    {args[1], args[2], plus_exprt(args[2], args[3])},
+    loc,
+    symbol_table,
+    code);
+
+  // Assign string_expr to `this` object
+  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
+  code.add(
+    code_assign_string_expr_to_java_string(
+      arg_this, string_expr, symbol_table));
+
+  return code;
+}
+
 /// Generates code for the String.length method
 /// \param type: type of the function
 /// \param loc: location in the source
@@ -1788,12 +1841,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
         std::placeholders::_1,
         std::placeholders::_2,
         std::placeholders::_3);
-  cprover_equivalent_to_java_constructor
-    ["java::java.lang.String.<init>:([C)V"]=
-      ID_cprover_string_copy_func;
-  cprover_equivalent_to_java_constructor
-    ["java::java.lang.String.<init>:([CII)V"]=
-      ID_cprover_string_copy_func;
+  conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
+    &java_string_library_preprocesst::make_init_from_array_code,
+    this,
+    std::placeholders::_1,
+    std::placeholders::_2,
+    std::placeholders::_3);
   cprover_equivalent_to_java_constructor
     ["java::java.lang.String.<init>:()V"]=
       ID_cprover_string_empty_string_func;

src/java_bytecode/java_string_library_preprocess.h

@@ -323,6 +323,11 @@ class java_string_library_preprocesst:public messaget
     code_blockt &code);
 
   exprt get_object_at_index(const exprt &argv, int index);
+
+  codet make_init_from_array_code(
+    const code_typet &type,
+    const source_locationt &loc,
+    symbol_tablet &symbol_table);
 };
 
 exprt make_function_application(