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 () | |
![]() | |
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 | signature |
irep_idt | name |
bool | is_public |
bool | is_protected |
bool | is_private |
bool | is_static |
bool | is_final |
annotationst | annotations |
Definition at line 71 of file java_bytecode_parse_tree.h.
typedef std::vector<exceptiont> java_bytecode_parse_treet::methodt::exception_tablet |
Definition at line 96 of file java_bytecode_parse_tree.h.
typedef std::vector<instructiont> java_bytecode_parse_treet::methodt::instructionst |
Definition at line 78 of file java_bytecode_parse_tree.h.
typedef std::vector<local_variablet> java_bytecode_parse_treet::methodt::local_variable_tablet |
Definition at line 109 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 146 of file java_bytecode_parse_tree.h.
|
inline |
Definition at line 151 of file java_bytecode_parse_tree.h.
|
inline |
Definition at line 81 of file java_bytecode_parse_tree.h.
References instructions.
|
virtual |
Implements java_bytecode_parse_treet::membert.
Definition at line 115 of file java_bytecode_parse_tree.cpp.
References expr2java(), and from_expr().
irep_idt java_bytecode_parse_treet::methodt::base_name |
Definition at line 74 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 97 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert_instructions(), and java_bytecode_parsert::rmethod_attribute().
instructionst java_bytecode_parse_treet::methodt::instructions |
Definition at line 79 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 75 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_native |
Definition at line 75 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 75 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 110 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_convert_methodt::convert(), 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 76 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 147 of file java_bytecode_parse_tree.h.
Referenced by java_bytecode_parsert::rcode_attribute().