1/*******************************************************************\
3Module: JAVA Bytecode Language Conversion
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
12#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
13#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
24 &local_variable_table,
32 size_t max_array_length,
33 bool throw_assertion_error,
34 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
37 bool threading_support,
38 const std::optional<prefix_filtert> &method_context,
39 bool assert_no_exceptions_thrown);
85#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Non-graph-based representation of the class hierarchy.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::vector< parametert > parameterst
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
The symbol table base class interface.
The type of an expression, extends irept.
void java_bytecode_convert_method_lazy(symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &, symbol_table_baset &symbol_table, message_handlert &)
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.
expanding_vectort< std::vector< java_bytecode_convert_methodt::variablet > > variablest
void create_parameter_symbols(const java_method_typet::parameterst ¶meters, variablest &variables, symbol_table_baset &symbol_table)
Adds the parameter symbols to the symbol table.
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 sym...
void create_parameter_names(const java_bytecode_parse_treet::methodt &m, const irep_idt &method_identifier, java_method_typet::parameterst ¶meters, const java_bytecode_convert_methodt::method_offsett &slots_for_parameters)
Extracts the names of parameters from the local variable table in the method, and uses it to construc...
void create_method_stub_symbol(const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, const typet &type, const irep_idt &declaring_class, symbol_table_baset &symbol_table, message_handlert &message_handler)
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)
JAVA Bytecode Language Conversion.
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
std::vector< local_variablet > local_variable_tablet