java_bytecode_parse_treet::methodt::verification_type_infot Struct Reference

#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

Detailed Description

Definition at line 139 of file java_bytecode_parse_tree.h.

Member Enumeration Documentation

verification_type_info_type

enum java_bytecode_parse_treet::methodt::verification_type_infot::verification_type_info_type

Enumerator
TOP
INTEGER
FLOAT
LONG
DOUBLE
ITEM_NULL
UNINITIALIZED_THIS
OBJECT
UNINITIALIZED

Definition at line 141 of file java_bytecode_parse_tree.h.

Member Data Documentation

cpool_index

u2 java_bytecode_parse_treet::methodt::verification_type_infot::cpool_index

Definition at line 146 of file java_bytecode_parse_tree.h.

offset

u2 java_bytecode_parse_treet::methodt::verification_type_infot::offset

Definition at line 147 of file java_bytecode_parse_tree.h.

tag

u1 java_bytecode_parse_treet::methodt::verification_type_infot::tag

Definition at line 145 of file java_bytecode_parse_tree.h.

type

verification_type_info_type java_bytecode_parse_treet::methodt::verification_type_infot::type

Definition at line 144 of file java_bytecode_parse_tree.h.

---

The documentation for this struct was generated from the following file:

• /builddir/build/BUILD/cbmc-6.4.1-build/cbmc-cbmc-6.4.1/jbmc/src/java_bytecode/java_bytecode_parse_tree.h