java_bytecode_convert_methodt::holet Struct Reference

#include <java_bytecode_convert_method_class.h>

Public Attributes
unsigned	start_pc
unsigned	length

Detailed Description

Definition at line 95 of file java_bytecode_convert_method_class.h.

Member Data Documentation

length

unsigned java_bytecode_convert_methodt::holet::length

Definition at line 98 of file java_bytecode_convert_method_class.h.

start_pc

unsigned java_bytecode_convert_methodt::holet::start_pc

Definition at line 97 of file java_bytecode_convert_method_class.h.

---

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

• /builddir/build/BUILD/cbmc-cbmc-5.10/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h