cprover
|
JAVA Bytecode Language Conversion. More...
#include "ci_lazy_methods_needed.h"
#include "java_bytecode_parse_tree.h"
#include "java_string_library_preprocess.h"
#include <util/message.h>
#include <util/symbol_table.h>
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... | |
JAVA Bytecode Language Conversion.
Definition in file java_bytecode_convert_method.h.
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 3065 of file java_bytecode_convert_method.cpp.
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.
class_symbol | The class this method belongs to |
method_identifier | The fully qualified method name, including type descriptor (e.g. "x.y.z.f:(I)") |
m | The parsed method object to convert. |
symbol_table | The global symbol table (will be modified). |
message_handler | A message handler to collect warnings. |
Definition at line 337 of file java_bytecode_convert_method.cpp.
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.
method_symbol | The symbol for the method for which to initialize the parameters |
local_variable_table | The local variable table containing the bytecode for the parameters |
symbol_table | The symbol table into which to insert symbols for the parameters |
Definition at line 2987 of file java_bytecode_convert_method.cpp.