7.2.6 ClassInvariant Attribute

This attribute describes the class invariant. It has the following structure:

     ClassInvariant_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       formula_info invariant;
     }

[alx: this seems to correspond to JMLClassInvariant_attribute from D3.1, but the format is different]

The meaning of the fields is the following:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.ClassInvariant)
• attribute_length - length in bytes of the whole structure
• invariant - the binary representation of the invariant formula.