Add function_name parameter to process_operands

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

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -265,13 +265,15 @@ symbol_exprt java_string_library_preprocesst::fresh_array(
 /// calls string_refine_preprocesst::process_operands with a list of parameters.
 /// \param params: a list of function parameters
 /// \param loc: location in the source
+/// \param function_name: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \param init_code: code block, in which declaration of some arguments may be
 ///   added
 /// \return a list of expressions
 exprt::operandst java_string_library_preprocesst::process_parameters(
   const java_method_typet::parameterst &params,
   const source_locationt &loc,
+  const irep_idt &function_name,
   symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
@@ -281,7 +283,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
     const symbol_exprt sym(p.get_identifier(), p.type());
     ops.push_back(sym);
   }
-  return process_operands(ops, loc, symbol_table, init_code);
+  return process_operands(ops, loc, function_name, symbol_table, init_code);
 }
 
 /// Creates a string_exprt from the input exprt representing a char sequence
@@ -322,23 +324,24 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 /// for char array references.
 /// \param operands: a list of expressions
 /// \param loc: location in the source
+/// \param function_name: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \param init_code: code block, in which declaration of some arguments may be
 ///   added
 /// \return a list of expressions
 exprt::operandst java_string_library_preprocesst::process_operands(
   const exprt::operandst &operands,
   const source_locationt &loc,
+  const irep_idt &function_name,
   symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
   exprt::operandst ops;
   for(const auto &p : operands)
   {
     if(implements_java_char_sequence_pointer(p.type()))
-      ops.push_back(
-        convert_exprt_to_string_exprt(
-          p, loc, symbol_table, loc.get_function(), init_code));
+      ops.push_back(convert_exprt_to_string_exprt(
+        p, loc, symbol_table, function_name, 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
@@ -1128,7 +1131,7 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call(
 
   // Processing parameters
   const exprt::operandst args =
-    process_parameters(params, loc, symbol_table, code);
+    process_parameters(params, loc, function_name, symbol_table, code);
 
   // string_expr <- function(arg1)
   const refined_string_exprt string_expr =
@@ -1472,8 +1475,8 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
 {
   PRECONDITION(type.parameters().size()==2);
   code_blockt code;
-  exprt::operandst args=process_parameters(
-    type.parameters(), loc, symbol_table, code);
+  exprt::operandst args =
+    process_parameters(type.parameters(), loc, function_id, symbol_table, code);
   INVARIANT(args.size()==2, "String.format should have two arguments");
 
   // The argument can be:
@@ -1612,8 +1615,8 @@ code_blockt java_string_library_preprocesst::make_function_from_call(
   symbol_table_baset &symbol_table)
 {
   code_blockt code;
-  const exprt::operandst args =
-    process_parameters(type.parameters(), loc, symbol_table, code);
+  const exprt::operandst args = process_parameters(
+    type.parameters(), loc, function_name, symbol_table, code);
   code.add(
     code_return_function_application(
       function_name, args, type.return_type(), symbol_table),
@@ -1645,8 +1648,8 @@ java_string_library_preprocesst::make_string_returning_function_from_call(
   code_blockt code;
 
   // Calling the function
-  const exprt::operandst arguments =
-    process_parameters(type.parameters(), loc, symbol_table, code);
+  const exprt::operandst arguments = process_parameters(
+    type.parameters(), loc, function_name, symbol_table, code);
 
   // String expression that will hold the result
   const refined_string_exprt string_expr =

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -185,6 +185,7 @@ class java_string_library_preprocesst:public messaget
   exprt::operandst process_parameters(
     const java_method_typet::parameterst &params,
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
@@ -206,6 +207,7 @@ class java_string_library_preprocesst:public messaget
   exprt::operandst process_operands(
     const exprt::operandst &operands,
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &init_code);