Add function_id parameter to decl_string_expr

This is in preparation for giving function_id as an argument to the
function creating fresh java symbols.

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -306,7 +306,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, function_id, symbol_table, init_code);
   code_assign_java_string_to_string_expr(
     string_expr, expr_to_process, loc, symbol_table, init_code);
   return string_expr;
@@ -496,11 +496,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_id: name of the function in which the string is defined
 /// \param symbol_table: the symbol table
 /// \param [out] code: 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_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -542,7 +544,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, function_id, symbol_table, code);
 
   const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
@@ -1672,7 +1675,7 @@ code_blockt 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, function_id, symbol_table, code);
 
   // Assign the argument to string_expr
   const java_method_typet::parametert &op = type.parameters()[0];
@@ -1719,7 +1722,7 @@ code_blockt 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

@@ -233,6 +233,7 @@ class java_string_library_preprocesst:public messaget
 
   refined_string_exprt decl_string_expr(
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
@@ -250,13 +251,13 @@ class java_string_library_preprocesst:public messaget
     code_blockt &code);
 
   codet code_return_function_application(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const exprt::operandst &arguments,
     const typet &type,
     symbol_table_baset &symbol_table);
 
   refined_string_exprt string_expr_of_function(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const exprt::operandst &arguments,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
@@ -289,32 +290,32 @@ class java_string_library_preprocesst:public messaget
     code_blockt &code);
 
   code_blockt make_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_init_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
     bool is_constructor = true);
 
   code_blockt make_assign_and_return_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_assign_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_string_returning_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);