cprover
|
#include <java_bytecode_parse_tree.h>
Classes | |
struct | exceptiont |
class | local_variablet |
class | stack_map_table_entryt |
class | 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 () |
virtual void | output (std::ostream &out) const |
methodt () | |
virtual | ~methodt ()=default |
![]() | |
membert () | |
Public Attributes | |
irep_idt | base_name |
bool | is_native |
bool | is_abstract |
bool | is_synchronized |
source_locationt | source_location |
instructionst | instructions |
exception_tablet | 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 89 of file java_bytecode_parse_tree.h.
typedef std::vector<exceptiont> java_bytecode_parse_treet::methodt::exception_tablet |
Definition at line 119 of file java_bytecode_parse_tree.h.
typedef std::vector<instructiont> java_bytecode_parse_treet::methodt::instructionst |
Definition at line 96 of file java_bytecode_parse_tree.h.
typedef std::vector<local_variablet> java_bytecode_parse_treet::methodt::local_variable_tablet |
Definition at line 133 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 170 of file java_bytecode_parse_tree.h.
|
inline |
Definition at line 175 of file java_bytecode_parse_tree.h.
|
virtualdefault |
|
inline |
Definition at line 99 of file java_bytecode_parse_tree.h.
References instructions.
|
virtual |
Implements java_bytecode_parse_treet::membert.
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 92 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 120 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 97 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 93 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_native |
Definition at line 93 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 93 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_parsert::rmethod().
local_variable_tablet java_bytecode_parse_treet::methodt::local_variable_table |
Definition at line 134 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 94 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 171 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_parsert::rcode_attribute().