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, bool threading_support)
 
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,
bool  threading_support 
)

Definition at line 3050 of file java_bytecode_convert_method.cpp.

◆ 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_symbolThe class this method belongs to
method_identifierThe fully qualified method name, including type descriptor (e.g. "x.y.z.f:(I)")
mThe parsed method object to convert.
symbol_tableThe global symbol table (will be modified).
message_handlerA message handler to collect warnings.

Definition at line 336 of file java_bytecode_convert_method.cpp.

◆ 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 2972 of file java_bytecode_convert_method.cpp.