cprover
|
Public Types | |
typedef java_bytecode_parse_treet::classt | classt |
typedef java_bytecode_parse_treet::fieldt | fieldt |
Public Member Functions | |
java_bytecode_convert_classt (symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, lazy_methodst &_lazy_methods, lazy_methods_modet _lazy_methods_mode, bool _string_refinement_enabled, const character_refine_preprocesst &_character_preprocess) | |
void | operator() (const java_bytecode_parse_treet &parse_tree) |
Protected Member Functions | |
void | convert (const classt &c) |
void | convert (symbolt &class_symbol, const fieldt &f) |
void | generate_class_stub (const irep_idt &class_name) |
void | add_array_types () |
void | add_string_type () |
Implements the java.lang.String type in the case that we provide an internal implementation. More... | |
Protected Attributes | |
symbol_tablet & | symbol_table |
const size_t | max_array_length |
lazy_methodst & | lazy_methods |
lazy_methods_modet | lazy_methods_mode |
bool | string_refinement_enabled |
character_refine_preprocesst | character_preprocess |
Additional Inherited Members |
Definition at line 29 of file java_bytecode_convert_class.cpp.
Definition at line 63 of file java_bytecode_convert_class.cpp.
Definition at line 64 of file java_bytecode_convert_class.cpp.
|
inline |
Definition at line 32 of file java_bytecode_convert_class.cpp.
|
protected |
Definition at line 275 of file java_bytecode_convert_class.cpp.
References symbol_tablet::add(), symbolt::base_name, struct_union_typet::components(), irept::get(), symbol_typet::get_identifier(), symbolt::is_type, java_array_type(), java_int_type(), java_type_from_char(), symbolt::name, pointer_type(), struct_union_typet::set_tag(), symbol_table, to_symbol_type(), and symbolt::type.
Referenced by operator()().
|
protected |
Implements the java.lang.String type in the case that we provide an internal implementation.
Definition at line 354 of file java_bytecode_convert_class.cpp.
References symbol_tablet::add(), class_typet::add_base(), symbolt::base_name, struct_union_typet::components(), symbolt::is_type, java_boolean_type(), java_char_type(), java_int_type(), java_reference_type(), symbolt::mode, symbolt::name, code_typet::parameters(), pointer_type(), symbolt::pretty_name, code_typet::return_type(), struct_union_typet::set_tag(), code_typet::parametert::set_this(), symbol_table, symbolt::type, and exprt::type().
Referenced by operator()().
|
protected |
Definition at line 83 of file java_bytecode_convert_class.cpp.
References class_typet::add_base(), symbolt::base_name, character_preprocess, struct_union_typet::components(), messaget::debug(), dstringt::empty(), java_bytecode_parse_treet::classt::enum_elements, messaget::eom(), messaget::error(), java_bytecode_parse_treet::classt::extends, java_bytecode_parse_treet::classt::fields, messaget::get_message_handler(), symbol_tablet::has_symbol(), id2string(), java_bytecode_parse_treet::classt::implements, java_bytecode_parse_treet::classt::is_enum, symbolt::is_type, java_bytecode_convert_method(), java_bytecode_convert_method_lazy(), java_root_class(), lazy_methods, lazy_methods_mode, LAZY_METHODS_MODE_EAGER, max_array_length, java_bytecode_parse_treet::classt::methods, symbolt::mode, symbol_tablet::move(), symbolt::name, java_bytecode_parse_treet::classt::name, symbolt::pretty_name, irept::set(), struct_union_typet::componentt::set_base_name(), struct_union_typet::componentt::set_name(), struct_union_typet::componentt::set_pretty_name(), struct_union_typet::set_tag(), symbol_table, symbolt::type, and exprt::type().
Referenced by operator()().
Definition at line 214 of file java_bytecode_convert_class.cpp.
References symbol_tablet::add(), symbolt::base_name, struct_union_typet::components(), messaget::get_message_handler(), id2string(), symbolt::is_lvalue, java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, symbolt::is_state_var, java_bytecode_parse_treet::membert::is_static, symbolt::is_static_lifetime, symbolt::is_type, java_type_from_string(), symbolt::location, symbolt::mode, symbolt::name, java_bytecode_parse_treet::membert::name, symbolt::pretty_name, struct_union_typet::componentt::set_access(), struct_union_typet::componentt::set_base_name(), struct_union_typet::componentt::set_name(), struct_union_typet::componentt::set_pretty_name(), java_bytecode_parse_treet::membert::signature, symbol_table, symbol_tablet::symbols, to_class_type(), symbolt::type, exprt::type(), symbolt::value, and zero_initializer().
|
protected |
Definition at line 180 of file java_bytecode_convert_class.cpp.
References symbolt::base_name, messaget::eom(), id2string(), symbolt::is_type, java_root_class(), symbolt::mode, symbol_tablet::move(), symbolt::name, symbolt::pretty_name, irept::set(), struct_union_typet::set_tag(), symbol_table, symbolt::type, and messaget::warning().
Referenced by operator()().
|
inline |
Definition at line 50 of file java_bytecode_convert_class.cpp.
References add_array_types(), add_string_type(), convert(), generate_class_stub(), java_bytecode_parse_treet::loading_successful, java_bytecode_parse_treet::classt::name, java_bytecode_parse_treet::parsed_class, and string_refinement_enabled.
|
protected |
Definition at line 72 of file java_bytecode_convert_class.cpp.
Referenced by convert().
|
protected |
Definition at line 69 of file java_bytecode_convert_class.cpp.
Referenced by convert().
|
protected |
Definition at line 70 of file java_bytecode_convert_class.cpp.
Referenced by convert().
|
protected |
Definition at line 68 of file java_bytecode_convert_class.cpp.
Referenced by convert().
|
protected |
Definition at line 71 of file java_bytecode_convert_class.cpp.
Referenced by operator()().
|
protected |
Definition at line 67 of file java_bytecode_convert_class.cpp.
Referenced by add_array_types(), add_string_type(), convert(), and generate_class_stub().