7.2.6 ClassInvariant Attribute

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

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

The meaning of the fields is as follows:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.ClassInvariant)
• attribute_length - length in bytes of the whole structure
• access_flags - the flags that are set for the invariant. The only allowed flags are ACC_PUBLIC, ACC_PROTECTED, ACC_PRIVATE and ACC_STATIC. All other flags must be cleared. Only one of ACC_PUBLIC, ACC_PROTECTED, ACC_PRIVATE can be set.
• invariant - the binary representation of the invariant formula.