CBMC
|
#include <java_bytecode_parse_tree.h>
Public Types | |
enum | verification_type_info_type { TOP , INTEGER , FLOAT , LONG , DOUBLE , ITEM_NULL , UNINITIALIZED_THIS , OBJECT , UNINITIALIZED } |
Public Attributes | |
verification_type_info_type | type |
u1 | tag |
u2 | cpool_index |
u2 | offset |
Definition at line 139 of file java_bytecode_parse_tree.h.
Enumerator | |
---|---|
TOP | |
INTEGER | |
FLOAT | |
LONG | |
DOUBLE | |
ITEM_NULL | |
UNINITIALIZED_THIS | |
OBJECT | |
UNINITIALIZED |
Definition at line 141 of file java_bytecode_parse_tree.h.
u2 java_bytecode_parse_treet::methodt::verification_type_infot::cpool_index |
Definition at line 146 of file java_bytecode_parse_tree.h.
u2 java_bytecode_parse_treet::methodt::verification_type_infot::offset |
Definition at line 147 of file java_bytecode_parse_tree.h.
u1 java_bytecode_parse_treet::methodt::verification_type_infot::tag |
Definition at line 145 of file java_bytecode_parse_tree.h.
verification_type_info_type java_bytecode_parse_treet::methodt::verification_type_infot::type |
Definition at line 144 of file java_bytecode_parse_tree.h.