cprover
java_bytecode_convert_method.h File Reference

JAVA Bytecode Language Conversion. More...

Include dependency graph for java_bytecode_convert_method.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void java_bytecode_initialize_parameter_names (symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
 This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode. More...
 
void java_bytecode_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy)
 
void java_bytecode_convert_method_lazy (const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table, message_handlert &)
 This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet. More...
 

Detailed Description

JAVA Bytecode Language Conversion.

Definition in file java_bytecode_convert_method.h.

Function Documentation

◆ java_bytecode_convert_method()

void java_bytecode_convert_method ( const symbolt class_symbol,
const java_bytecode_parse_treet::methodt ,
symbol_table_baset symbol_table,
message_handlert message_handler,
size_t  max_array_length,
bool  throw_assertion_error,
optionalt< ci_lazy_methods_neededt needed_lazy_methods,
java_string_library_preprocesst string_preprocess,
const class_hierarchyt class_hierarchy 
)

◆ java_bytecode_convert_method_lazy()

void java_bytecode_convert_method_lazy ( const symbolt class_symbol,
const irep_idt method_identifier,
const java_bytecode_parse_treet::methodt m,
symbol_tablet symbol_table,
message_handlert message_handler 
)

This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.

The caller should call java_bytecode_convert_method later to give the symbol/method a body.

parameters: class_symbol: class this method belongs to
method_identifier: fully qualified method name, including type descriptor (e.g. "x.y.z.f:(I)") m: parsed method object to convert symbol_table: global symbol table (will be modified) message_handler: message handler to collect warnings

Definition at line 338 of file java_bytecode_convert_method.cpp.

References symbol_table_baset::add(), java_bytecode_parse_treet::membert::annotations, symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, convert_annotations(), java_bytecode_parse_treet::membert::descriptor, java_bytecode_parse_treet::find_annotation(), id2string(), java_bytecode_parse_treet::methodt::is_abstract, is_constructor(), java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_reference_type(), symbolt::location, member_type_lazy(), message_handler, symbolt::mode, symbolt::name, code_typet::parameters(), symbolt::pretty_name, pretty_signature(), irept::set(), code_typet::set_access(), source_locationt::set_function(), code_typet::set_is_constructor(), code_typet::parametert::set_this(), java_bytecode_parse_treet::membert::signature, java_bytecode_parse_treet::methodt::source_location, symbolt::type, and exprt::type().

◆ java_bytecode_initialize_parameter_names()

void java_bytecode_initialize_parameter_names ( symbolt method_symbol,
const java_bytecode_parse_treet::methodt::local_variable_tablet local_variable_table,
symbol_table_baset symbol_table 
)

This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode.

Remarks
This is useful for pre-initialization for methods generated by the string solver
Parameters
method_symbolThe symbol for the method for which to initialize the parameters
local_variable_tableThe local variable table containing the bytecode for the parameters
symbol_tableThe symbol table into which to insert symbols for the parameters

Definition at line 3007 of file java_bytecode_convert_method.cpp.

References symbolt::base_name, id2string(), symbol_table_baset::insert(), java_char_from_type(), java_local_variable_slots(), java_method_parameter_slots(), symbolt::mode, symbolt::name, code_typet::parameters(), to_code_type(), to_string(), and symbolt::type.

Referenced by java_bytecode_languaget::convert_single_method().