12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H 13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H 27 &local_variable_table,
35 size_t max_array_length,
36 bool throw_assertion_error,
40 bool threading_support);
49 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H Non-graph-based representation of the class hierarchy.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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...
nonstd::optional< T > optionalt
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
The symbol table base class interface.
std::vector< local_variablet > local_variable_tablet
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...
Context-insensitive lazy methods container.
goto_programt coverage_criteriont 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, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)
Produce code for simple implementation of String Java libraries.