Java string preprocessing: Remove or document unused parameter function_id

Author: tautschnig

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -628,7 +628,7 @@ codet initialize_nondet_string_struct(
     // data_expr = nondet(char[INFINITY]) // we use infinity for variable size
     const dereference_exprt data_expr(data_pointer);
     const exprt nondet_array =
-      make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
+      make_nondet_infinite_char_array(symbol_table, loc, code);
     code.add(code_assignt(data_expr, nondet_array));
 
     struct_expr.copy_to_operands(length_expr);

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -539,7 +539,6 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
 /// \return a new string_expr
 refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   const source_locationt &loc,
-  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -550,7 +549,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   code.add(code_assignt(str.length(), nondet_length), loc);
 
   exprt nondet_array_expr =
-    make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
+    make_nondet_infinite_char_array(symbol_table, loc, code);
 
   address_of_exprt array_pointer(
     index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
@@ -652,7 +651,6 @@ codet java_string_library_preprocesst::code_return_function_application(
 exprt make_nondet_infinite_char_array(
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
-  const irep_idt &function_id,
   code_blockt &code)
 {
   const array_typet array_type(
@@ -805,7 +803,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   code.add(code_declt(return_code), loc);
 
   const refined_string_exprt string_expr =
-    make_nondet_string_expr(loc, function_name, symbol_table, code);
+    make_nondet_string_expr(loc, symbol_table, code);
 
   // args is { str.length, str.content, arguments... }
   exprt::operandst args;
@@ -940,6 +938,7 @@ java_string_library_preprocesst::string_literal_to_string_expr(
 /// \param type: type of the function call
 /// \param loc: location in the program_invocation_name
 /// \param symbol_table: symbol table
+/// \param function_id: unused
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// IF arg->@class_identifier == "java.lang.String"
@@ -957,6 +956,8 @@ codet java_string_library_preprocesst::make_equals_function_code(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
+  (void)function_id;
+
   const typet &return_type = type.return_type();
   exprt::operandst ops;
   for(const auto &p : type.parameters())
@@ -1416,7 +1417,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
     }
     else
       field_expr =
-        make_nondet_string_expr(loc, function_id, symbol_table, code);
+        make_nondet_string_expr(loc, symbol_table, code);
 
     field_exprs.push_back(field_expr);
     arg_i_struct.copy_to_operands(field_expr);
@@ -1735,6 +1736,7 @@ codet java_string_library_preprocesst::make_copy_string_code(
 /// object.
 /// \param type: type of the function
 /// \param loc: location in the source
+/// \param function_id: unused
 /// \param symbol_table: symbol table
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1748,6 +1750,8 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
+  (void)function_id;
+
   // Code for the output
   code_blockt code;
 
@@ -1774,6 +1778,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
 /// count instead of end index
 /// \param type: type of the function call
 /// \param loc: location in the program_invocation_name
+/// \param function_id: unused
 /// \param symbol_table: symbol table
 /// \return code implementing String intitialization from a char array and
 ///         arguments offset and end.
@@ -1783,6 +1788,8 @@ codet java_string_library_preprocesst::make_init_from_array_code(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
+  (void)function_id;
+
   // Code for the output
   code_blockt code;
 
@@ -1818,6 +1825,7 @@ codet java_string_library_preprocesst::make_init_from_array_code(
 /// Generates code for the String.length method
 /// \param type: type of the function
 /// \param loc: location in the source
+/// \param function_id: unused
 /// \param symbol_table: symbol table
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1831,6 +1839,9 @@ codet java_string_library_preprocesst::make_string_length_code(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
+  (void)loc;
+  (void)function_id;
+
   code_typet::parameterst params=type.parameters();
   symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
   dereference_exprt deref=

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -249,7 +249,6 @@ class java_string_library_preprocesst:public messaget
 
   refined_string_exprt make_nondet_string_expr(
     const source_locationt &loc,
-    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
@@ -363,7 +362,6 @@ class java_string_library_preprocesst:public messaget
 exprt make_nondet_infinite_char_array(
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
-  const irep_idt &function_id,
   code_blockt &code);
 
 void add_pointer_to_array_association(