cprover
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 "ci_lazy_methods_needed.h"
18 
19 #include <util/message.h>
20 #include <util/symbol_table.h>
21 
22 class class_hierarchyt;
23 
25  symbolt &method_symbol,
27  &local_variable_table,
28  symbol_table_baset &symbol_table);
29 
31  const symbolt &class_symbol,
33  symbol_table_baset &symbol_table,
34  message_handlert &message_handler,
35  size_t max_array_length,
36  bool throw_assertion_error,
37  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
38  java_string_library_preprocesst &string_preprocess,
39  const class_hierarchyt &class_hierarchy,
40  bool threading_support);
41 
43  const symbolt &class_symbol,
44  const irep_idt &method_identifier,
46  symbol_tablet &symbol_table,
48 
49 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)
Definition: java_bytecode_convert_method.cpp:3065
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:86
java_string_library_preprocess.h
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:2987
java_bytecode_parse_tree.h
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
ci_lazy_methods_needed.h
message_handlert
Definition: message.h:24
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_bytecode_parse_treet::methodt::local_variable_tablet
std::vector< local_variablet > local_variable_tablet
Definition: java_bytecode_parse_tree.h:138
symbolt
Symbol table entry.
Definition: symbol.h:27
java_bytecode_convert_method_lazy
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.
Definition: java_bytecode_convert_method.cpp:337
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:35
symbol_table.h
Author: Diffblue Ltd.
message.h