CBMC
java_bytecode_convert_method.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
14 
15 #include "java_bytecode_convert_method_class.h"
16 #include "java_bytecode_parse_tree.h"
17 
18 class class_hierarchyt;
19 class prefix_filtert;
20 
21 void java_bytecode_initialize_parameter_names(
22  symbolt &method_symbol,
23  const java_bytecode_parse_treet::methodt::local_variable_tablet
24  &local_variable_table,
25  symbol_table_baset &symbol_table);
26 
27 void java_bytecode_convert_method(
28  const symbolt &class_symbol,
29  const java_bytecode_parse_treet::methodt &,
30  symbol_table_baset &symbol_table,
31  message_handlert &message_handler,
32  size_t max_array_length,
33  bool throw_assertion_error,
34  std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
35  java_string_library_preprocesst &string_preprocess,
36  const class_hierarchyt &class_hierarchy,
37  bool threading_support,
38  const std::optional<prefix_filtert> &method_context,
39  bool assert_no_exceptions_thrown);
40 
41 void create_method_stub_symbol(
42  const irep_idt &identifier,
43  const irep_idt &base_name,
44  const irep_idt &pretty_name,
45  const typet &type,
46  const irep_idt &declaring_class,
47  symbol_table_baset &symbol_table,
48  message_handlert &message_handler);
49 
50 void java_bytecode_convert_method_lazy(
51  symbolt &class_symbol,
52  const irep_idt &method_identifier,
53  const java_bytecode_parse_treet::methodt &,
54  symbol_table_baset &symbol_table,
55  message_handlert &);
56 
57 typedef expanding_vectort<std::vector<java_bytecode_convert_methodt::variablet>>
58  variablest;
59 
70 void create_parameter_names(
71  const java_bytecode_parse_treet::methodt &m,
72  const irep_idt &method_identifier,
73  java_method_typet::parameterst &parameters,
74  const java_bytecode_convert_methodt::method_offsett &slots_for_parameters);
75 
80 void create_parameter_symbols(
81  const java_method_typet::parameterst &parameters,
82  variablest &variables,
83  symbol_table_baset &symbol_table);
84 
85 #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:27
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