Add function_name argument to decl_string_expr

This is in preparation for giving function_name as an argument to the
function creating new string objects.

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -305,7 +305,11 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 {
   PRECONDITION(implements_java_char_sequence_pointer(expr_to_process.type()));
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, symbol_table, init_code);
+    decl_string_expr(
+      loc,
+      loc.get_function(),
+      symbol_table,
+      init_code);
   code_assign_java_string_to_string_expr(
     string_expr, expr_to_process, loc, symbol_table, init_code);
   return string_expr;
@@ -497,6 +501,7 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
 /// \return refined string expr with fresh content and length symbols
 refined_string_exprt java_string_library_preprocesst::decl_string_expr(
   const source_locationt &loc,
+  const irep_idt &function_name,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -538,7 +543,11 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   code_blockt &code)
 {
   /// \todo refactor with initialize_nonddet_string_struct
-  const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
+  const refined_string_exprt str = decl_string_expr(
+    loc,
+    loc.get_function(),
+    symbol_table,
+    code);
 
   const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
@@ -1648,7 +1657,11 @@ codet java_string_library_preprocesst::make_copy_string_code(
 
   // String expression that will hold the result
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, symbol_table, code);
+    decl_string_expr(
+      loc,
+      loc.get_function(),
+      symbol_table,
+      code);
 
   // Assign the argument to string_expr
   const java_method_typet::parametert op = type.parameters()[0];
@@ -1693,7 +1706,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
 
   // String expression that will hold the result
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, symbol_table, code);
+    decl_string_expr(loc, function_id, symbol_table, code);
 
   // Assign argument to a string_expr
   const java_method_typet::parameterst params = type.parameters();

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -232,6 +232,7 @@ class java_string_library_preprocesst:public messaget
 
   refined_string_exprt decl_string_expr(
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &code);