Conflicting JVM specs between what can be verified run and what is debuggable wrt local variables?

On one hand the Java class spec says:

There may be no more than one LocalVariableTable attribute per local variable in the attributes table of a Code attribute.

But on the other hand lots of research papers ponder the problem that at JVM bytecode verification (and execution) level you can have conflicting types for a local variable in different regions of a method. E.g. Leroy (2003)

The least upper bound of two types for a register (or stack slot) can be 'top', causing this register to have type 'top' in the merged state. This corresponds to the situation where a register holds values of incompatible types in two arms of a conditional (e.g. int in one arm and an object reference in the other), and therefore is treated as uninitialized (no further loads from this register) after the merge point.

So, does that mean the JVM spec for the debugging info is partly broken, in that it cannot represent debugging info in such [complex] cases, where the local variable is reused with a different type in the same method? (Those would need multiple records in the LocalVariableTable, one for each range that has a different type. But the spec seem to forbid that.)

Of course, the verification algorithm has changed substantially (from type inference described in that [2003] paper) to type checking using StackMapTables for class version >= 50. Does the latter prohibit the situation from the 2nd quote? (And if so, is the spec conflict between what's verifiable and what's debuggable [local-variables wise] limited to class version <= 49?)

N.B. It's easy [at least for me!] to sometimes confuse the requirements for the stack with those for the local variables. While on merging even JDK 1.0 required the stack to have identical types (except for refs), that's not the case with local variables. From the very first JMV spec (1996):

To merge two local variable states, corresponding pairs of local variables are compared. If the two types are not identical, then unless both contain reference values, the verifier records that the local variable contains an unusable value. If both of the pair of local variables contain reference values, the merged state contains a reference to an instance of the first common superclass of the two types.

That sentence/para is nearly identical e.g. in JDK 11 spec:

To merge two local variable array states, corresponding pairs of local variables are compared. The value of the merged local variable is computed using the rules above, except that the corresponding values are permitted to be different primitive types. In that case, the verifier records that the merged local variable contains an unusable value.

However this doesn't cause verification to fail (unlike the similar situation with stacks) at least in the spec.

So, what Leroy wrote checks out against the JVM spec. Thus, since it's valid bytecode to have different types for the same locals on branches, unless you later read from that local, my question remains valid: is that situation not representable in the LocalVariableTable, for debugging purposes?

The subject of the sentence is “LocalVariableTable attribute”, not “entry within the LocalVariableTable attribute”. The rather surprising information that more than one LocalVariableTable attribute is allowed at a Code attribute is already hinted in the preceding sentence:

If multiple LocalVariableTable attributes are present in the attributes table of a Code attribute, then they may appear in any order.

The specified limit of “at most one LocalVariableTable attribute per local variable” is of little relevance in practice, given that one LocalVariableTable attribute is sufficient to describe all local variables of a method. I’ve never seen multiple LocalVariableTable attributes at a method in real life and just verified that not even libraries like the widely used ASM library are prepared to handle multiple LocalVariableTable attributes at one method.

The HotSpot JVM, however, does accept multiple LocalVariableTable attributes at a Code attribute (I just checked this) and verifies that there are no duplicate entries throughout all of them. But “duplicate entry” means “entry with the same combination of start_pc, length, name, and index” here and just altering one of those value made the JVM accept it, despite being contradicting. On the other hand, it’s not clear why the JVM enforces a constraint not explicitly mentioned in the specification, in an optional debug attribute, in the first place.