Loading...
Searching...
No Matches
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.
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.
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, std::optional<
ci_lazy_methods_neededt > needed_lazy_methods,
java_string_library_preprocesst &string_preprocess,
const class_hierarchyt &class_hierarchy,
bool threading_support,
const std::optional<
prefix_filtert > &method_context,
bool assert_no_exceptions_thrown)
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.
Extracts the names of parameters from the local variable table in the method, and uses it to construct sensible names/identifiers for the parameters in the parameters on the
java_method_typet and the external variables vector.
Adds the parameter symbols to the symbol table.
Detailed Description
Typedef Documentation
◆ variablest
Function Documentation
◆ create_method_stub_symbol()
◆ create_parameter_names()
Extracts the names of parameters from the local variable table in the method, and uses it to construct sensible names/identifiers for the parameters in the parameters on the java_method_typet and the external variables vector.
- Parameters
-
m the parsed method whose local variable table contains the name of the parameters
method_identifier the identifier of the method
slots_for_parameters the number of parameter slots available, i.e. a positive integer
Definition at line 422 of file java_bytecode_convert_method.cpp.
◆ create_parameter_symbols()
Adds the parameter symbols to the symbol table.
- Parameters
-
variables external storage of jvm variables [out]
symbol_table the symbol table [out]
◆ java_bytecode_convert_method()
bool
throw_assertion_error,
bool
assert_no_exceptions_thrown
)
◆ java_bytecode_convert_method_lazy()
void java_bytecode_convert_method_lazy
(
symbolt &
class_symbol,
)
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 The class this method belongs to. The method, if not static, will be added to the class' list of methods.
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 299 of file java_bytecode_convert_method.cpp.
◆ java_bytecode_initialize_parameter_names()
void java_bytecode_initialize_parameter_names
(
symbolt &
method_symbol,
)
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_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 3203 of file java_bytecode_convert_method.cpp.
