cprover
|
Public Types | |
typedef java_bytecode_parse_treet::classt | classt |
typedef java_bytecode_parse_treet::fieldt | fieldt |
typedef java_bytecode_parse_treet::methodt | methodt |
typedef java_bytecode_parse_treet::annotationt | annotationt |
Public Member Functions | |
java_bytecode_convert_classt (symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &_string_preprocess, const std::unordered_set< std::string > &no_load_classes) | |
void | operator() (const java_class_loadert::parse_tree_with_overlayst &parse_trees) |
Converts all the class parse trees into a class symbol and adds it to the symbol table. More... | |
Private Types | |
typedef std::list< std::reference_wrapper< const classt > > | overlay_classest |
Private Member Functions | |
void | convert (const classt &c, const overlay_classest &overlay_classes) |
Convert a class, adding symbols to the symbol table for its members. More... | |
void | convert (symbolt &class_symbol, const fieldt &f) |
Convert a field, adding a symbol to teh symbol table for it. More... | |
bool | check_field_exists (const fieldt &field, const irep_idt &qualified_fieldname, const struct_union_typet::componentst &fields) const |
Static Private Member Functions | |
static void | add_array_types (symbol_tablet &symbol_table) |
Register in the symbol_table new symbols for the objects java::array[X] where X is byte, float, int, char... More... | |
static bool | is_overlay_method (const methodt &method) |
static bool | is_ignored_method (const methodt &method) |
Private Attributes | |
symbol_tablet & | symbol_table |
const size_t | max_array_length |
method_bytecodet & | method_bytecode |
java_string_library_preprocesst & | string_preprocess |
std::unordered_set< std::string > | no_load_classes |
Additional Inherited Members |
Definition at line 31 of file java_bytecode_convert_class.cpp.
Definition at line 105 of file java_bytecode_convert_class.cpp.
Definition at line 102 of file java_bytecode_convert_class.cpp.
Definition at line 103 of file java_bytecode_convert_class.cpp.
Definition at line 104 of file java_bytecode_convert_class.cpp.
|
private |
Definition at line 114 of file java_bytecode_convert_class.cpp.
|
inline |
Definition at line 34 of file java_bytecode_convert_class.cpp.
|
staticprivate |
Register in the symbol_table
new symbols for the objects java::array[X] where X is byte, float, int, char...
Definition at line 723 of file java_bytecode_convert_class.cpp.
Referenced by operator()().
|
private |
Definition at line 569 of file java_bytecode_convert_class.cpp.
|
private |
Convert a class, adding symbols to the symbol table for its members.
c | Bytecode of the class to convert |
overlay_classes | Bytecode of any overlays for the class to convert |
Definition at line 230 of file java_bytecode_convert_class.cpp.
References class_typet::add_base(), class_typet::bases(), struct_union_typet::components(), messaget::debug(), dstringt::empty(), java_bytecode_parse_treet::classt::enum_elements, messaget::eom(), extract_generic_interface_reference(), extract_generic_superclass_reference(), java_generic_class_typet::generic_types(), symbol_table_baset::has_symbol(), id2string(), java_bytecode_parse_treet::classt::implements, java_bytecode_parse_treet::classt::is_abstract, java_bytecode_parse_treet::classt::is_annotation, java_bytecode_parse_treet::classt::is_anonymous_class, java_bytecode_parse_treet::classt::is_enum, java_bytecode_parse_treet::classt::is_final, java_bytecode_parse_treet::classt::is_inner_class, java_bytecode_parse_treet::classt::is_interface, java_bytecode_parse_treet::classt::is_private, java_bytecode_parse_treet::classt::is_protected, java_bytecode_parse_treet::classt::is_public, java_bytecode_parse_treet::classt::is_static_class, java_bytecode_parse_treet::classt::is_synthetic, java_generic_type_from_string(), max_array_length, java_bytecode_parse_treet::classt::name, java_bytecode_parse_treet::classt::outer_class, irept::set(), java_class_typet::set_access(), struct_union_typet::componentt::set_base_name(), java_class_typet::set_final(), java_class_typet::set_is_anonymous_class(), java_class_typet::set_is_inner_class(), java_class_typet::set_is_static_class(), struct_union_typet::componentt::set_name(), java_class_typet::set_outer_class(), struct_union_typet::componentt::set_pretty_name(), java_class_typet::set_super_class(), struct_union_typet::set_tag(), java_bytecode_parse_treet::classt::signature, java_bytecode_parse_treet::classt::super_class, symbol_table, to_java_generic_parameter(), to_string(), exprt::type(), and messaget::warning().
Referenced by operator()().
Convert a field, adding a symbol to teh symbol table for it.
class_symbol | The already added symbol for the containing class |
f | The bytecode for the field to convert |
this is for a free type variable, e.g., a field of the form T f;
this is for a field that holds a generic type, either with instantiated or with free type variables, e.g., List<T> l;
or List<Integer> l;
Definition at line 590 of file java_bytecode_convert_class.cpp.
|
inlinestaticprivate |
Definition at line 126 of file java_bytecode_convert_class.cpp.
References java_bytecode_parse_treet::membert::has_annotation().
|
inlinestaticprivate |
Definition at line 121 of file java_bytecode_convert_class.cpp.
References java_bytecode_parse_treet::membert::has_annotation().
|
inline |
Converts all the class parse trees into a class symbol and adds it to the symbol table.
parse_trees | The parse trees found for the class to be converted. |
\@java::com.diffblue.OverlayClassImplementation
. Overlay class definitions can contain methods with the same signature as methods in the original class, so long as these are marked with the attribute \@java::com.diffblue.OverlayMethodImplementation
; such overlay methods are replaced in the original file with the version found in the last overlay on the classpath. Later definitions can also contain new supporting methods and fields that are merged in. This will allow insertion of Java methods into library classes to handle, for example, modelling dependency injection. Definition at line 65 of file java_bytecode_convert_class.cpp.
References add_array_types(), java_string_library_preprocesst::add_string_type(), convert(), generate_class_stub(), messaget::get_message_handler(), id2string(), java_string_library_preprocesst::is_known_string_type(), no_load_classes, PRECONDITION, string_preprocess, and symbol_table.
|
private |
Definition at line 109 of file java_bytecode_convert_class.cpp.
Referenced by convert().
|
private |
Definition at line 110 of file java_bytecode_convert_class.cpp.
|
private |
Definition at line 136 of file java_bytecode_convert_class.cpp.
Referenced by operator()().
|
private |
Definition at line 111 of file java_bytecode_convert_class.cpp.
Referenced by operator()().
|
private |
Definition at line 108 of file java_bytecode_convert_class.cpp.
Referenced by convert(), and operator()().