java__bytecode__convert__method_8h_source.html

 /*******************************************************************\


 Module: JAVA Bytecode Language Conversion


 Author: Daniel Kroening, kroening@kroening.com


 \*******************************************************************/


 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H

 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H


 #include "java_bytecode_convert_method_class.h"

 #include "java_bytecode_parse_tree.h"


 class class_hierarchyt;

 class prefix_filtert;


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


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


 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_lazy(

   symbolt &class_symbol,

   const irep_idt &method_identifier,

   const java_bytecode_parse_treet::methodt &,

   symbol_table_baset &symbol_table,

   message_handlert &);


 typedef expanding_vectort<std::vector<java_bytecode_convert_methodt::variablet>>

   variablest;


 void create_parameter_names(

   const java_bytecode_parse_treet::methodt &m,

   const irep_idt &method_identifier,

   java_method_typet::parameterst &parameters,

   const java_bytecode_convert_methodt::method_offsett &slots_for_parameters);


 void create_parameter_symbols(

   const java_method_typet::parameterst &parameters,

   variablest &variables,

   symbol_table_baset &symbol_table);


 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H

class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:41

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38

expanding_vectort
Definition: expanding_vector.h:17

java_bytecode_convert_methodt::method_offsett
uint16_t method_offsett
Definition: java_bytecode_convert_method_class.h:77

java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:585

java_string_library_preprocesst
Definition: java_string_library_preprocess.h:38

message_handlert
Definition: message.h:28

prefix_filtert
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
Definition: prefix_filter.h:20

symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23

symbolt
Symbol table entry.
Definition: symbol.h:28

typet
The type of an expression, extends irept.
Definition: type.h:29

java_bytecode_convert_method_lazy
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.
Definition: java_bytecode_convert_method.cpp:299

variablest
expanding_vectort< std::vector< java_bytecode_convert_methodt::variablet > > variablest
Definition: java_bytecode_convert_method.h:58

create_parameter_symbols
void create_parameter_symbols(const java_method_typet::parameterst &parameters, variablest &variables, symbol_table_baset &symbol_table)
Adds the parameter symbols to the symbol table.

java_bytecode_initialize_parameter_names
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...
Definition: java_bytecode_convert_method.cpp:3200

create_parameter_names
void create_parameter_names(const java_bytecode_parse_treet::methodt &m, const irep_idt &method_identifier, java_method_typet::parameterst &parameters, 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...
Definition: java_bytecode_convert_method.cpp:422

create_method_stub_symbol
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)
Definition: java_bytecode_convert_method.cpp:94

java_bytecode_convert_method
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)
Definition: java_bytecode_convert_method.cpp:3278

java_bytecode_convert_method_class.h
JAVA Bytecode Language Conversion.

java_bytecode_parse_tree.h

declaring_class
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:568

java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:85

java_bytecode_parse_treet::methodt::local_variable_tablet
std::vector< local_variablet > local_variable_tablet
Definition: java_bytecode_parse_tree.h:136