cprover
|
#include <java_bytecode_parse_tree.h>
Classes | |
class | annotationt |
class | classt |
class | fieldt |
class | instructiont |
class | membert |
class | methodt |
Public Types | |
typedef std::vector< annotationt > | annotationst |
typedef std::set< irep_idt > | class_refst |
Public Member Functions | |
java_bytecode_parse_treet (const java_bytecode_parse_treet &)=delete | |
java_bytecode_parse_treet & | operator= (const java_bytecode_parse_treet &)=delete |
java_bytecode_parse_treet (java_bytecode_parse_treet &&)=default | |
java_bytecode_parse_treet & | operator= (java_bytecode_parse_treet &&)=default |
virtual | ~java_bytecode_parse_treet ()=default |
void | output (std::ostream &out) const |
java_bytecode_parse_treet () | |
Static Public Member Functions | |
static optionalt< annotationt > | find_annotation (const annotationst &annotations, const irep_idt &annotation_type_name) |
Find an annotation given its name. More... | |
Public Attributes | |
classt | parsed_class |
class_refst | class_refs |
bool | loading_successful |
Definition at line 22 of file java_bytecode_parse_tree.h.
typedef std::vector<annotationt> java_bytecode_parse_treet::annotationst |
Definition at line 55 of file java_bytecode_parse_tree.h.
typedef std::set<irep_idt> java_bytecode_parse_treet::class_refst |
Definition at line 300 of file java_bytecode_parse_tree.h.
|
delete |
|
default |
|
virtualdefault |
|
inline |
Definition at line 305 of file java_bytecode_parse_tree.h.
|
static |
Find an annotation given its name.
annotations | A vector of annotationt |
annotation_type_name | An irep_idt representing the name of the annotation class, e.g. java::java.lang.SuppressWarnings |
Definition at line 109 of file java_bytecode_parse_tree.cpp.
References symbol_typet::get_identifier(), irept::id(), typet::subtype(), and to_symbol_type().
Referenced by is_overlay_class(), and java_bytecode_convert_method_lazy().
|
delete |
|
default |
void java_bytecode_parse_treet::output | ( | std::ostream & | out | ) | const |
Definition at line 21 of file java_bytecode_parse_tree.cpp.
References class_refs, java_bytecode_parse_treet::classt::output(), and parsed_class.
class_refst java_bytecode_parse_treet::class_refs |
Definition at line 301 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_parsert::get_class_refs(), java_bytecode_parsert::get_class_refs_rec(), output(), and java_bytecode_parsert::rclass_attribute().
bool java_bytecode_parse_treet::loading_successful |
Definition at line 303 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_parsert::rClassFile().
classt java_bytecode_parse_treet::parsed_class |
Definition at line 295 of file java_bytecode_parse_tree.h.
Referenced by create_stub_global_symbols(), ci_lazy_methodst::entry_point_methods(), generate_constant_global_variables(), java_bytecode_parsert::get_class_refs(), java_class_loadert::get_parse_tree(), infer_opaque_type_fields(), output(), java_bytecode_parsert::rClassFile(), and java_bytecode_parsert::rmethod_attribute().