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,7 @@ 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;
@@ -492,11 +492,13 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
 /// Add declaration of a refined string expr whose content and length are
 /// fresh symbols.
 /// \param loc: source location
+/// \param function_name: name of the function in which the stirng is defined
 /// \param symbol_table: the symbol table
 /// \param code [out] : code block to which the declaration is added
 /// \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 +540,8 @@ 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);
@@ -1654,7 +1657,7 @@ 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];
@@ -1699,7 +1702,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);