Merge pull request #2483 from tautschnig/vs-java-parameters

Java front-end: remove unused parameters

Author: peterschrammel

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -619,8 +619,6 @@ void java_bytecode_convert_methodt::convert(
   if((!m.is_abstract) && (!m.is_native))
     method_symbol.value = convert_instructions(
       m,
-      method_type,
-      method_symbol.name,
       to_java_class_type(class_symbol.type).lambda_method_handles());
 }
 
@@ -989,8 +987,6 @@ static std::size_t get_bytecode_type_width(const typet &ty)
 
 codet java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
-  const code_typet &method_type,
-  const irep_idt &method_name,
   const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
 {
   const instructionst &instructions=method.instructions;
@@ -3151,7 +3147,6 @@ bool java_bytecode_convert_methodt::is_method_inherited(
     get_inherited_component(
       classname,
       methodid,
-      classname,
       symbol_table,
       class_hierarchy,
       false);
@@ -3171,7 +3166,6 @@ irep_idt java_bytecode_convert_methodt::get_static_field(
     get_inherited_component(
       class_identifier,
       component_name,
-      symbol_table.lookup_ref(current_method).type.get(ID_C_class),
       symbol_table,
       class_hierarchy,
       true);

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -268,8 +268,6 @@ class java_bytecode_convert_methodt:public messaget
 
   codet convert_instructions(
     const methodt &,
-    const code_typet &,
-    const irep_idt &,
     const java_class_typet::java_lambda_method_handlest &);
 
   const bytecode_infot &get_bytecode_info(const irep_idt &statement);

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -549,7 +549,6 @@ static void create_stub_global_symbols(
           get_inherited_component(
             class_id,
             component,
-            "java::" + id2string(parse_tree.parsed_class.name),
             symbol_table,
             class_hierarchy,
             true);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -120,7 +120,6 @@ class java_object_factoryt
   void gen_nondet_pointer_init(
     code_blockt &assignments,
     const exprt &expr,
-    const irep_idt &class_identifier,
     allocation_typet alloc_type,
     const pointer_typet &pointer_type,
     size_t depth,
@@ -670,9 +669,6 @@ bool initialize_nondet_string_fields(
 ///   The code block we are building with initialization code.
 /// \param expr:
 ///   Pointer-typed lvalue expression to initialize.
-/// \param class_identifier:
-///   Name of the parent class. Used to initialize the `@class_identifier` among
-///   others.
 /// \param alloc_type:
 ///   Allocation type (global, local or dynamic)
 /// \param depth:
@@ -688,7 +684,6 @@ bool initialize_nondet_string_fields(
 void java_object_factoryt::gen_nondet_pointer_init(
   code_blockt &assignments,
   const exprt &expr,
-  const irep_idt &class_identifier,
   allocation_typet alloc_type,
   const pointer_typet &pointer_type,
   size_t depth,
@@ -1149,7 +1144,6 @@ void java_object_factoryt::gen_nondet_init(
     gen_nondet_pointer_init(
       assignments,
       expr,
-      class_identifier,
       alloc_type,
       pointer_type,
       depth,

jbmc/src/java_bytecode/java_utils.cpp

@@ -331,9 +331,6 @@ std::string pretty_print_java_type(const std::string &fqn_java_type)
 ///   trying to resolve a reference to A.b, component_class_id is "A".
 /// \param component_name: component basename to search for. If searching for
 ///   A.b, this is "b".
-/// \param user_class_id: class identifier making reference to the sought
-///   component. The user class is relevant when determining whether package-
-///   scoped components are visible from a particular use site.
 /// \param symbol_table: global symbol table.
 /// \param class_hierarchy: global class hierarchy.
 /// \param include_interfaces: if true, search for the given component in all
@@ -343,7 +340,6 @@ std::string pretty_print_java_type(const std::string &fqn_java_type)
 resolve_inherited_componentt::inherited_componentt get_inherited_component(
   const irep_idt &component_class_id,
   const irep_idt &component_name,
-  const irep_idt &user_class_id,
   const symbol_tablet &symbol_table,
   const class_hierarchyt &class_hierarchy,
   bool include_interfaces)

jbmc/src/java_bytecode/java_utils.h

@@ -103,7 +103,6 @@ std::string pretty_print_java_type(const std::string &fqn_java_type);
 resolve_inherited_componentt::inherited_componentt get_inherited_component(
   const irep_idt &component_class_id,
   const irep_idt &component_name,
-  const irep_idt &user_class_id,
   const symbol_tablet &symbol_table,
   const class_hierarchyt &class_hierarchy,
   bool include_interfaces);

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -21,6 +21,7 @@
 /// \param pointer_type: The pointer type replace
 /// \param generic_parameter_specialization_map map of types for all generic
 /// parameters in the current scope
+/// \param ns Namespace for type lookups
 /// \return A pointer type where the subtype may have been modified
 pointer_typet select_pointer_typet::convert_pointer_type(
   const pointer_typet &pointer_type,