cprover
|
Classes | |
class | bytecodet |
struct | pool_entryt |
Public Member Functions | |
java_bytecode_parsert (bool skip_instructions) | |
virtual bool | parse () |
![]() | |
virtual void | clear () |
parsert () | |
virtual | ~parsert () |
bool | read (char &ch) |
bool | eof () |
void | parse_error (const std::string &message, const std::string &before) |
void | inc_line_no () |
void | set_line_no (unsigned _line_no) |
void | set_file (const irep_idt &file) |
irep_idt | get_file () const |
unsigned | get_line_no () const |
unsigned | get_column () const |
void | set_column (unsigned _column) |
void | set_source_location (exprt &e) |
void | set_function (const irep_idt &function) |
void | advance_column (unsigned token_width) |
Public Attributes | |
java_bytecode_parse_treet | parse_tree |
constant_poolt | constant_pool |
![]() | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
Protected Member Functions | |
pool_entryt & | pool_entry (u2 index) |
exprt & | constant (u2 index) |
const typet | type_entry (u2 index) |
void | populate_bytecode_mnemonics_table () |
void | rClassFile () |
void | rconstant_pool () |
void | rinterfaces (classt &parsed_class) |
void | rfields (classt &parsed_class) |
void | rmethods (classt &parsed_class) |
void | rmethod (classt &parsed_class) |
void | rinner_classes_attribute (classt &parsed_class, const u4 &attribute_length) |
Corresponds to the element_value structure Described in Java 8 specification 4.7.6 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6 Parses the InnerClasses attribute for the current parsed class, which contains an array of information about its inner classes. More... | |
std::vector< irep_idt > | rexceptions_attribute () |
Corresponds to the element_value structure Described in Java 8 specification 4.7.5 https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.5 Parses the Exceptions attribute for the current method, and returns a vector of exceptions. More... | |
void | rclass_attribute (classt &parsed_class) |
void | rRuntimeAnnotation_attribute (annotationst &) |
void | rRuntimeAnnotation (annotationt &) |
void | relement_value_pairs (annotationt::element_value_pairst &) |
exprt | get_relement_value () |
Corresponds to the element_value structure Described in Java 8 specification 4.7.16.1 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1. More... | |
void | rmethod_attribute (methodt &method) |
void | rfield_attribute (fieldt &) |
void | rcode_attribute (methodt &method) |
void | read_verification_type_info (methodt::verification_type_infot &) |
void | rbytecode (methodt::instructionst &) |
void | get_class_refs () |
Get the class references for the benefit of a dependency analysis. More... | |
void | get_class_refs_rec (const typet &) |
void | get_annotation_class_refs (const java_bytecode_parse_treet::annotationst &annotations) |
For each of the given annotations, get a reference to its class and recursively get class references of the values it stores. More... | |
void | get_annotation_value_class_refs (const exprt &value) |
See java_bytecode_parsert::get_annotation_class_refs. More... | |
void | parse_local_variable_type_table (methodt &method) |
Parses the local variable type table of a method. More... | |
optionalt< lambda_method_handlet > | parse_method_handle (const class method_handle_infot &entry) |
Read method handle pointed to from constant pool entry at index, return type of method handle and name if lambda function is found. More... | |
void | read_bootstrapmethods_entry (classt &) |
Read all entries of the BootstrapMethods attribute of a class file. More... | |
void | skip_bytes (std::size_t bytes) |
u8 | read_bytes (size_t bytes) |
u1 | read_u1 () |
u2 | read_u2 () |
u4 | read_u4 () |
u8 | read_u8 () |
void | store_unknown_method_handle (classt &parsed_class, size_t bootstrap_method_index, u2_valuest u2_values) const |
Creates an unknown method handle and puts it into the parsed_class. More... | |
Protected Attributes | |
std::vector< bytecodet > | bytecodes |
const bool | skip_instructions = false |
![]() | |
source_locationt | source_location |
unsigned | line_no |
unsigned | previous_line_no |
unsigned | column |
Additional Inherited Members |
Definition at line 32 of file java_bytecode_parser.cpp.
Definition at line 51 of file java_bytecode_parser.cpp.
Definition at line 50 of file java_bytecode_parser.cpp.
Definition at line 43 of file java_bytecode_parser.cpp.
typedef std::vector<pool_entryt> java_bytecode_parsert::constant_poolt |
Definition at line 70 of file java_bytecode_parser.cpp.
Definition at line 44 of file java_bytecode_parser.cpp.
Definition at line 47 of file java_bytecode_parser.cpp.
Definition at line 48 of file java_bytecode_parser.cpp.
Definition at line 49 of file java_bytecode_parser.cpp.
typedef java_bytecode_parse_treet::classt::lambda_method_handlet java_bytecode_parsert::lambda_method_handlet |
Definition at line 55 of file java_bytecode_parser.cpp.
typedef java_bytecode_parse_treet::classt::method_handle_typet java_bytecode_parsert::method_handle_typet |
Definition at line 53 of file java_bytecode_parser.cpp.
Definition at line 45 of file java_bytecode_parser.cpp.
Definition at line 46 of file java_bytecode_parser.cpp.
Definition at line 56 of file java_bytecode_parser.cpp.
|
inlineexplicit |
Definition at line 35 of file java_bytecode_parser.cpp.
Definition at line 96 of file java_bytecode_parser.cpp.
|
protected |
For each of the given annotations, get a reference to its class and recursively get class references of the values it stores.
Definition at line 656 of file java_bytecode_parser.cpp.
|
protected |
See java_bytecode_parsert::get_annotation_class_refs.
For the different cases of exprt
, see java_bytecode_parsert::get_relement_value.
Definition at line 670 of file java_bytecode_parser.cpp.
|
protected |
Get the class references for the benefit of a dependency analysis.
Definition at line 539 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 622 of file java_bytecode_parser.cpp.
|
protected |
Corresponds to the element_value structure Described in Java 8 specification 4.7.16.1 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1.
Definition at line 1586 of file java_bytecode_parser.cpp.
|
virtual |
Implements parsert.
Definition at line 430 of file java_bytecode_parser.cpp.
|
protected |
Parses the local variable type table of a method.
The LVTT holds generic type information for variables in the local variable table (LVT). At most as many variables as present in the LVT can be in the LVTT.
Definition at line 1911 of file java_bytecode_parser.cpp.
|
protected |
Read method handle pointed to from constant pool entry at index, return type of method handle and name if lambda function is found.
entry | the constant pool entry of the methodhandle_info structure |
Definition at line 1953 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 84 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 106 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 954 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1741 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 475 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1337 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 689 of file java_bytecode_parser.cpp.
|
protected |
Read all entries of the BootstrapMethods
attribute of a class file.
parsed_class | the class representation of the class file that is currently parsed |
Definition at line 1996 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 165 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 181 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 186 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 191 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 196 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1505 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1566 of file java_bytecode_parser.cpp.
|
protected |
Corresponds to the element_value structure Described in Java 8 specification 4.7.5 https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.5 Parses the Exceptions attribute for the current method, and returns a vector of exceptions.
Definition at line 1726 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1316 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 913 of file java_bytecode_parser.cpp.
|
protected |
Corresponds to the element_value structure Described in Java 8 specification 4.7.6 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6 Parses the InnerClasses attribute for the current parsed class, which contains an array of information about its inner classes.
We are interested in getting information only for inner classes, which is determined by checking if the parsed class matches any of the inner classes in its inner class array. If the parsed class is not an inner class, then it is ignored. When a parsed class is an inner class, the accessibility information for the parsed class is overwritten, and the parsed class is marked as an inner class.
Definition at line 1651 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 904 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1837 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1217 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1814 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1558 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 1545 of file java_bytecode_parser.cpp.
|
inlineprotected |
Definition at line 152 of file java_bytecode_parser.cpp.
|
protected |
Creates an unknown method handle and puts it into the parsed_class.
parsed_class | The class whose bootstrap method handles we are using |
bootstrap_method_index | The current index in the bootstrap entry table |
u2_values | The indices of the arguments for the call |
Definition at line 2139 of file java_bytecode_parser.cpp.
Definition at line 101 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 81 of file java_bytecode_parser.cpp.
constant_poolt java_bytecode_parsert::constant_pool |
Definition at line 71 of file java_bytecode_parser.cpp.
java_bytecode_parse_treet java_bytecode_parsert::parse_tree |
Definition at line 58 of file java_bytecode_parser.cpp.
|
protected |
Definition at line 82 of file java_bytecode_parser.cpp.