Java string preprocessing: Remove or document unused parameter function_id

Author: tautschnig

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -635,7 +635,7 @@ bool initialize_nondet_string_fields(
   // 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.operands()[struct_type.component_number("length")] = length_expr;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -540,7 +540,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)
 {
@@ -551,7 +550,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())));
@@ -653,7 +652,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(
@@ -806,7 +804,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;
@@ -941,6 +939,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"
@@ -958,6 +957,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())
@@ -1417,7 +1418,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);
@@ -1736,6 +1737,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:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1749,6 +1751,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;
 
@@ -1775,6 +1779,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.
@@ -1784,6 +1789,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;
 
@@ -1819,6 +1826,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:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1832,6 +1840,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(