cprover
|
Classes | |
struct | pool_entryt |
Public Member Functions | |
java_bytecode_parsert (bool skip_instructions, message_handlert &message_handler) | |
bool | parse () override |
Public Member Functions inherited from parsert | |
parsert (message_handlert &message_handler) | |
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) |
const source_locationt & | source_location () |
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 |
Public Attributes inherited from parsert | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
Private Types | |
using | classt = java_bytecode_parse_treet::classt |
using | methodt = java_bytecode_parse_treet::methodt |
using | fieldt = java_bytecode_parse_treet::fieldt |
using | instructiont = java_bytecode_parse_treet::instructiont |
using | annotationt = java_bytecode_parse_treet::annotationt |
using | method_handle_typet = java_class_typet::method_handle_kindt |
using | lambda_method_handlet |
using | constant_poolt = std::vector<pool_entryt> |
Private Member Functions | |
pool_entryt & | pool_entry (u2 index) |
exprt & | constant (u2 index) |
const typet | type_entry (u2 index) |
void | rClassFile () |
void | rconstant_pool () |
void | rinterfaces () |
void | rfields () |
void | rmethods () |
void | rmethod () |
void | rinner_classes_attribute (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. | |
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. | |
void | rclass_attribute () |
void | rRuntimeAnnotation_attribute (std::vector< annotationt > &) |
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. | |
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 (std::vector< instructiont > &) |
void | get_class_refs () |
Get the class references for the benefit of a dependency analysis. | |
void | get_class_refs_rec (const typet &) |
void | get_annotation_class_refs (const std::vector< annotationt > &annotations) |
For each of the given annotations, get a reference to its class and recursively get class references of the values it stores. | |
void | get_annotation_value_class_refs (const exprt &value) |
See java_bytecode_parsert::get_annotation_class_refs. | |
void | parse_local_variable_type_table (methodt &method) |
Parses the local variable type table of a method. | |
std::optional< 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. | |
void | read_bootstrapmethods_entry () |
Read all entries of the BootstrapMethods attribute of a class file. | |
void | skip_bytes (std::size_t bytes) |
template<typename T> | |
T | read () |
void | store_unknown_method_handle (size_t bootstrap_method_index) |
Creates an unknown method handle and puts it into the parsed_class. |
Private Attributes | |
constant_poolt | constant_pool |
const bool | skip_instructions = false |
Additional Inherited Members | |
Protected Attributes inherited from parsert | |
messaget | log |
source_locationt | _source_location |
unsigned | line_no |
unsigned | previous_line_no |
unsigned | column |
Definition at line 27 of file java_bytecode_parser.cpp.
Definition at line 56 of file java_bytecode_parser.cpp.
|
private |
Definition at line 52 of file java_bytecode_parser.cpp.
|
private |
Definition at line 61 of file java_bytecode_parser.cpp.
|
private |
Definition at line 54 of file java_bytecode_parser.cpp.
Definition at line 55 of file java_bytecode_parser.cpp.
|
private |
Definition at line 58 of file java_bytecode_parser.cpp.
Definition at line 57 of file java_bytecode_parser.cpp.
|
private |
Definition at line 53 of file java_bytecode_parser.cpp.
|
inline |
Definition at line 30 of file java_bytecode_parser.cpp.
Definition at line 81 of file java_bytecode_parser.cpp.
|
private |
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 621 of file java_bytecode_parser.cpp.
|
private |
See java_bytecode_parsert::get_annotation_class_refs.
For the different cases of exprt, see java_bytecode_parsert::get_relement_value.
Definition at line 635 of file java_bytecode_parser.cpp.
|
private |
Get the class references for the benefit of a dependency analysis.
Definition at line 506 of file java_bytecode_parser.cpp.
|
private |
Definition at line 591 of file java_bytecode_parser.cpp.
|
private |
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 1535 of file java_bytecode_parser.cpp.
|
overridevirtual |
Implements parsert.
Definition at line 392 of file java_bytecode_parser.cpp.
|
private |
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 1860 of file java_bytecode_parser.cpp.
|
private |
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 1930 of file java_bytecode_parser.cpp.
|
inlineprivate |
Definition at line 67 of file java_bytecode_parser.cpp.
|
private |
Definition at line 894 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1692 of file java_bytecode_parser.cpp.
|
private |
Definition at line 442 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1296 of file java_bytecode_parser.cpp.
|
private |
Definition at line 653 of file java_bytecode_parser.cpp.
|
inlineprivate |
Definition at line 132 of file java_bytecode_parser.cpp.
|
private |
Read all entries of the BootstrapMethods attribute of a class file.
Definition at line 1983 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1454 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1515 of file java_bytecode_parser.cpp.
|
private |
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 1677 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1275 of file java_bytecode_parser.cpp.
|
private |
Definition at line 853 of file java_bytecode_parser.cpp.
|
private |
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 1601 of file java_bytecode_parser.cpp.
|
private |
Definition at line 844 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1785 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1162 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1762 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1507 of file java_bytecode_parser.cpp.
|
private |
Definition at line 1494 of file java_bytecode_parser.cpp.
|
inlineprivate |
Definition at line 118 of file java_bytecode_parser.cpp.
|
private |
Creates an unknown method handle and puts it into the parsed_class.
bootstrap_method_index | The current index in the bootstrap entry table |
Definition at line 2119 of file java_bytecode_parser.cpp.
Definition at line 86 of file java_bytecode_parser.cpp.
|
private |
Definition at line 63 of file java_bytecode_parser.cpp.
java_bytecode_parse_treet java_bytecode_parsert::parse_tree |
Definition at line 49 of file java_bytecode_parser.cpp.
|
private |
Definition at line 65 of file java_bytecode_parser.cpp.