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
Non-graph-based representation of the class hierarchy.
Symbol table entry.
Definition: symbol.h:27
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
Definition: optional.h:35
The symbol table.
Definition: symbol_table.h:19
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
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&#39;t actually perform method conversion just yet...
Context-insensitive lazy methods container.
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.