|
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 () | |
Public Member Functions inherited from java_bytecode_parse_treet::membert | |
| 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 |
Public Attributes inherited from java_bytecode_parse_treet::membert | |
| 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().