Remove use of make_string_length_code

This code was directly accessing the length field of the object instead
of calling a builtin_function.
This meant the solver was unaware of some code accessing the length of a
string and could lead to inconsistencies when the solver decides not to
add the constraints specific to this string.

Author: romainbrenguier

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1776,28 +1776,6 @@ codet java_string_library_preprocesst::make_init_from_array_code(
   return code;
 }
 
-/// Generates code for the String.length method
-/// \param type: type of the function
-/// \param loc: location in the source
-/// \param symbol_table: symbol table
-/// \return Code corresponding to:
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// str_expr = java_string_to_string_expr(this)
-/// str_expr_sym = str_expr
-/// return this->length
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-codet java_string_library_preprocesst::make_string_length_code(
-  const code_typet &type,
-  const source_locationt &loc,
-  symbol_table_baset &symbol_table)
-{
-  code_typet::parameterst params=type.parameters();
-  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
-  dereference_exprt deref=
-    checked_dereference(arg_this, arg_this.type().subtype());
-  return code_returnt(get_length(deref, symbol_table));
-}
-
 bool java_string_library_preprocesst::implements_function(
   const irep_idt &function_id) const
 {
@@ -2018,14 +1996,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_function
     ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
       ID_cprover_string_last_index_of_func;
-  conversion_table
+  cprover_equivalent_to_java_function
     ["java::java.lang.String.length:()I"]=
-      std::bind(
-        &java_string_library_preprocesst::make_string_length_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+      ID_cprover_string_length_func;
   cprover_equivalent_to_java_function
     ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
      "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
@@ -2178,14 +2151,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
      "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
-  conversion_table
+  cprover_equivalent_to_java_function
     ["java::java.lang.StringBuilder.length:()I"]=
-      std::bind(
-        &java_string_library_preprocesst::make_string_length_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
+    ID_cprover_string_length_func;
   cprover_equivalent_to_java_assign_function
     ["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
       ID_cprover_string_char_set_func;
@@ -2283,9 +2251,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_assign_and_return_function
     ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/"
      "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
-  conversion_table
+  cprover_equivalent_to_java_function
     ["java::java.lang.StringBuffer.length:()I"]=
-      conversion_table["java::java.lang.String.length:()I"];
+    ID_cprover_string_length_func;
   cprover_equivalent_to_java_assign_function
     ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
       ID_cprover_string_char_set_func;

src/java_bytecode/java_string_library_preprocess.h

@@ -175,11 +175,6 @@ class java_string_library_preprocesst:public messaget
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
-  codet make_string_length_code(
-    const code_typet &type,
-    const source_locationt &loc,
-    symbol_table_baset &symbol_table);
-
   codet make_object_get_class_code(
     const code_typet &type,
     const source_locationt &loc,