cprover
Loading...
Searching...
No Matches
java_bytecode_convert_method.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Language Conversion
4
5Author: 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
19
20#include <util/message.h>
21#include <util/symbol_table.h>
22
24class prefix_filtert;
25
27 symbolt &method_symbol,
29 &local_variable_table,
30 symbol_table_baset &symbol_table);
31
33 const symbolt &class_symbol,
35 symbol_table_baset &symbol_table,
36 message_handlert &message_handler,
37 size_t max_array_length,
38 bool throw_assertion_error,
39 optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
40 java_string_library_preprocesst &string_preprocess,
41 const class_hierarchyt &class_hierarchy,
42 bool threading_support,
43 const optionalt<prefix_filtert> &method_context,
44 bool assert_no_exceptions_thrown);
45
47 const irep_idt &identifier,
48 const irep_idt &base_name,
49 const irep_idt &pretty_name,
50 const typet &type,
52 symbol_table_baset &symbol_table,
53 message_handlert &message_handler);
54
56 symbolt &class_symbol,
57 const irep_idt &method_identifier,
59 symbol_tablet &symbol_table,
61
64
77 const irep_idt &method_identifier,
79 const java_bytecode_convert_methodt::method_offsett &slots_for_parameters);
80
86 const java_method_typet::parameterst &parameters,
87 variablest &variables,
88 symbol_table_baset &symbol_table);
89
90#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
Context-insensitive lazy methods container.
Non-graph-based representation of the class hierarchy.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
std::vector< parametert > parameterst
Definition std_types.h:542
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
The symbol table base class interface.
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
void java_bytecode_convert_method_lazy(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.
expanding_vectort< std::vector< java_bytecode_convert_methodt::variablet > > variablest
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, const optionalt< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)
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.
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...
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...
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)
JAVA Bytecode Language Conversion.
Produce code for simple implementation of String Java libraries.
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
nonstd::optional< T > optionalt
Definition optional.h:35
std::vector< local_variablet > local_variable_tablet
Author: Diffblue Ltd.