cprover
|
#include <java_bytecode_parse_tree.h>
Classes | |
struct | exceptiont |
struct | local_variablet |
struct | stack_map_table_entryt |
struct | verification_type_infot |
Public Types | |
typedef std::vector< instructiont > | instructionst |
typedef std::vector< exceptiont > | exception_tablet |
typedef std::vector< local_variablet > | local_variable_tablet |
typedef std::vector< stack_map_table_entryt > | stack_map_tablet |
Public Member Functions | |
instructiont & | add_instruction () |
void | output (std::ostream &out) const |
methodt () | |
![]() | |
membert () | |
bool | has_annotation (const irep_idt &annotation_id) const |
Public Attributes | |
irep_idt | base_name |
bool | is_native |
bool | is_abstract |
bool | is_synchronized |
bool | is_bridge |
source_locationt | source_location |
instructionst | instructions |
exception_tablet | exception_table |
std::vector< irep_idt > | throws_exception_table |
local_variable_tablet | local_variable_table |
stack_map_tablet | stack_map_table |
![]() | |
std::string | descriptor |
optionalt< std::string > | signature |
irep_idt | name |
bool | is_public |
bool | is_protected |
bool | is_private |
bool | is_static |
bool | is_final |
annotationst | annotations |
Definition at line 86 of file java_bytecode_parse_tree.h.
typedef std::vector<exceptiont> java_bytecode_parse_treet::methodt::exception_tablet |
Definition at line 114 of file java_bytecode_parse_tree.h.
typedef std::vector<instructiont> java_bytecode_parse_treet::methodt::instructionst |
Definition at line 92 of file java_bytecode_parse_tree.h.
typedef std::vector<local_variablet> java_bytecode_parse_treet::methodt::local_variable_tablet |
Definition at line 129 of file java_bytecode_parse_tree.h.
typedef std::vector<stack_map_table_entryt> java_bytecode_parse_treet::methodt::stack_map_tablet |
Definition at line 164 of file java_bytecode_parse_tree.h.
|
inline |
Definition at line 169 of file java_bytecode_parse_tree.h.
|
inline |
Definition at line 95 of file java_bytecode_parse_tree.h.
References instructions.
void java_bytecode_parse_treet::methodt::output | ( | std::ostream & | out | ) | const |
Definition at line 128 of file java_bytecode_parse_tree.cpp.
References expr2java(), and from_expr().
irep_idt java_bytecode_parse_treet::methodt::base_name |
Definition at line 88 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_convert_method_lazy(), and java_bytecode_parsert::rmethod().
exception_tablet java_bytecode_parse_treet::methodt::exception_table |
Definition at line 115 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::do_exception_handling(), and java_bytecode_parsert::rmethod_attribute().
instructionst java_bytecode_parse_treet::methodt::instructions |
Definition at line 93 of file java_bytecode_parse_tree.h.
Referenced by add_instruction(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_parsert::rcode_attribute(), and java_bytecode_parsert::rmethod_attribute().
bool java_bytecode_parse_treet::methodt::is_abstract |
Definition at line 89 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_convert_method_lazy(), and java_bytecode_parsert::rmethod().
bool java_bytecode_parse_treet::methodt::is_bridge |
Definition at line 89 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_method_lazy(), and java_bytecode_parsert::rmethod().
bool java_bytecode_parse_treet::methodt::is_native |
Definition at line 89 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_parsert::rmethod().
bool java_bytecode_parse_treet::methodt::is_synchronized |
Definition at line 89 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_method_lazy(), and java_bytecode_parsert::rmethod().
local_variable_tablet java_bytecode_parse_treet::methodt::local_variable_table |
Definition at line 130 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_parsert::parse_local_variable_type_table(), java_bytecode_parsert::rcode_attribute(), and java_bytecode_convert_methodt::setup_local_variables().
source_locationt java_bytecode_parse_treet::methodt::source_location |
Definition at line 90 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_convert_method_lazy(), and java_bytecode_parsert::rmethod_attribute().
stack_map_tablet java_bytecode_parse_treet::methodt::stack_map_table |
Definition at line 165 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_parsert::rcode_attribute().
std::vector<irep_idt> java_bytecode_parse_treet::methodt::throws_exception_table |
Definition at line 117 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_parsert::rmethod_attribute().