Add function_name parameter to convert_exprt_to_string_exprt

This is in preparation to giving the function_name to the function
generating fresh java symbols.

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -289,6 +289,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
 ///   sequence
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
+/// \param function_name: name of the function in which the code will be added
 /// \param init_code: code block, in which declaration will be added:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// char *cprover_string_content;
@@ -303,11 +304,12 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
   const exprt &expr_to_process,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
+  const irep_idt &function_name,
   code_blockt &init_code)
 {
   PRECONDITION(implements_java_char_sequence_pointer(expr_to_process.type()));
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, loc.get_function(), symbol_table, init_code);
+    decl_string_expr(loc, function_name, symbol_table, init_code);
   code_assign_java_string_to_string_expr(
     string_expr, expr_to_process, loc, symbol_table, init_code);
   return string_expr;
@@ -335,7 +337,8 @@ exprt::operandst java_string_library_preprocesst::process_operands(
   {
     if(implements_java_char_sequence_pointer(p.type()))
       ops.push_back(
-        convert_exprt_to_string_exprt(p, loc, symbol_table, init_code));
+        convert_exprt_to_string_exprt(
+          p, loc, symbol_table, loc.get_function(), init_code));
     else if(is_java_char_array_pointer_type(p.type()))
       ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
     else
@@ -367,14 +370,16 @@ java_string_library_preprocesst::process_equals_function_operands(
   PRECONDITION(implements_java_char_sequence_pointer(op0.type()));
 
   ops.push_back(
-    convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code));
+    convert_exprt_to_string_exprt(
+      op0, loc, symbol_table, loc.get_function(), init_code));
 
   // TODO: Manage the case where we have a non-String Object (this should
   // probably be handled upstream. At any rate, the following code should be
   // protected with assertions on the type of op1.
   const typecast_exprt tcast(op1, to_pointer_type(op0.type()));
   ops.push_back(
-    convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
+    convert_exprt_to_string_exprt(
+      tcast, loc, symbol_table, loc.get_function(), init_code));
   return ops;
 }
 

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -200,6 +200,7 @@ class java_string_library_preprocesst:public messaget
     const exprt &deref,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
+    const irep_idt &function_name,
     code_blockt &init_code);
 
   exprt::operandst process_operands(

jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp

@@ -25,14 +25,15 @@ refined_string_exprt convert_exprt_to_string_exprt_unit_test(
   code_blockt &init_code)
 {
   return preprocess.convert_exprt_to_string_exprt(
-    deref, loc, symbol_table, init_code);
+    deref, loc, symbol_table, loc.get_function(), init_code);
 }
 
 TEST_CASE("Convert exprt to string exprt")
 {
   GIVEN("A location, a string expression, and a symbol table")
   {
     source_locationt loc;
+    loc.set_function("function_name");
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);
     code_blockt code;