JVMS is unclear about the relationship between format checking of the Code and StackMapTable attributes, "constraints on JVM code" described in 4.9, and the two verification algorithms described in 4.10.

The intent seems to be as follows:

- The 'code' and 'exception_table' arrays of the Code attribute are left unparsed during format checking and validated during verification.

- The StackMapTable attribute of the Code attribute is entirely ignored until verification (other than ensuring that "at most one" StackMapTable attribute is present).

- 4.9 should be read as a set of constraints that will be enforced at verification time. Basic constraints on the contents of 'exception_table' and 'StackMapTable' are static constraints, despite being left out of 4.9.1.

- Verification, as defined by 4.10, proceeds in two phases: first, enforcing the static constraints of 4.9.1; and second, using one of two algorithms to enforce the structural constraints of 4.9.2.

- 4.10.1 and 4.10.2 should assume the static constraints of 4.9.1 are already satisfied, and are concerned only with enforcing the (more complex) structural constraints.

Some revisions to 4.9 and 4.10, particularly in their introductory framing, will help to clarify these expectations.

HotSpot is mostly consistent with this scheme, with a few anomalies:

- Some assertions about 'exception_table' are checked by format checking, depending (it seems) on whether they depend on parsing of the code array.

- Verification-time constraint failures involving the 'exceptions_table' array or 'StackMapTable' attribute throw a ClassFormatError rather than a VerifyError.

- The constant pool reference of an Object_variable_info type in a StackMapTable is validated in the first verification phase, while the code offset of Uninitialized_variable_info is not validated until the second verification phase. This can be observed with a version 50.0 class file: a bad Obejct_variable_info will cause a verification failure, while a bad Unintialized_variable_info is considered a recoverable error, triggering verification by type inference.

I propose tightening up the spec and then fixing these anomalies.