7.5.6 BlockSpecification Attribute

The BlockSpecification attribute contains the table of block specifications. It has the following structure:

     BlockSpecification_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 blocks_count;
       {
         u2 start_pc;
         u2 start_order;
         u2 end_pc;
         u2 end_order;
         spec_info spec;
       } blocks[blocks_count];
     }

[alx: no couterpart in D3.1]

The meaning of particular fields is the following:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.BlockSpecification)
• attribute_length - length in bytes of the whole structure
• blocks_count - the number of block specifications in the table
• blocks - the table of block specifications; the fields in each specification have the following meaning:
  • start_pc,end_pc - the start and end of the block in the method code
  • start_order,end_order - the position of the start and end of the specified block in BML declarations at code addresses start_pc/end_pc
  • spec - the specification of the block (precondition, regular and exceptional post-conditions, and assignable clause); the format and meaning of this field is described in The MethodSpecification attribute