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_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, safe_pointer< ci_lazy_methodst > lazy_methods, const character_refine_preprocesst &character_refine)
 
void java_bytecode_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, const character_refine_preprocesst &character_preprocess)
 
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)
 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() [1/2]

void java_bytecode_convert_method ( const symbolt class_symbol,
const java_bytecode_parse_treet::methodt ,
symbol_tablet symbol_table,
message_handlert message_handler,
size_t  max_array_length,
safe_pointer< ci_lazy_methodst lazy_methods,
const character_refine_preprocesst character_refine 
)

§ java_bytecode_convert_method() [2/2]

void java_bytecode_convert_method ( const symbolt class_symbol,
const java_bytecode_parse_treet::methodt method,
symbol_tablet symbol_table,
message_handlert message_handler,
size_t  max_array_length,
const character_refine_preprocesst character_preprocess 
)
inline

§ 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 
)

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 signature (e.g. "x.y.z.f:(I)") m: parsed method object to convert symbol_table: global symbol table (will be modified)

Definition at line 207 of file java_bytecode_convert_method.cpp.

References symbol_tablet::add(), symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, id2string(), 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(), java_type_from_string(), symbolt::location, symbolt::mode, symbolt::name, code_typet::parameters(), symbolt::pretty_name, irept::set(), source_locationt::set_function(), code_typet::parametert::set_this(), java_bytecode_parse_treet::membert::signature, java_bytecode_parse_treet::methodt::source_location, to_code_type(), symbolt::type, and exprt::type().

Referenced by java_bytecode_convert_classt::convert(), and java_bytecode_convert_method().