diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 1b976187797..63b2198431f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 6e1c9b45567..aa59a050f1b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/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); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 663eab78563..7d8ff0d17d3 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/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); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 22740f55d91..24939ebe1a0 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/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, diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 5d49710d02b..9e9f4f499ab 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/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) diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 1cc5c7727d4..dea8f1bf412 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/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); diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index b94fdfe1f7a..6059b1e5084 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/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,