Previous: Method Attributes, Up: Encoding of BML in Class File Format


7.7 Code Attributes

These attributes represent BML elements which are relevant for the implementation of a method. Thus they are irrelevant for abstract or native methods, or (non-model) methods declared in an interface.

Most attributes contain tables of BML elements which refer to some code instructions (e.g., a BML set instruction is located at a particular point in the method code). Since there may be more than one BML element related to a given point of the method code, each BML specification has an order field next to the pc field, specifying what is the relative position of a given BML specification in the sequence of BML specifications occurring at this pc. Order fields of different BML specifications must be different, they do not have to be consecutive numbers. BML specifications with smaller order values are assumed to appear before specifications with greated order values.

The attributes are as follows:

7.7.1 LocalVariableModifiersTable Attribute

The LocalVariableModifiersTable attribute represents the BML modifiers of local variables declared in the method code. The structure of the attribute is as follows:

     LocalVariableModifiersTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 local_variables_count;
       {
         u2 access_flags;
         u4 BML_flags;
         u2 index;
       } local_variables[local_variables_count];
     }

The meaning of the fields is as follows:

The format of this table is closely related to the information contained in the ParameterTable Attribute. Only local variables which are not parameters can be described here and each one at most once. Parameters should be described in the ParameterTable attribute.

The distinction between the two tables comes from the fact that parameters are part of the method specification and therefore they are valid e.g., in interfaces and abstract classes, while local variables are valid only in presence of the method's code and hence the Code attribute. Using this convention, to implement a method's specification one has to provide only the Code attribute. The specification, together with the information about parameters, remains unchanged.

This attribute, together with the ParameterTable attribute complement the information about local variables contained in the JVM LocalVariableTable Attribute.

7.7.2 LocalGhostVariableTable Attribute

This attribute describes the local ghost variables defined in the code. The structure of the attribute and the meaning of the fields is very similar to that of the LocalVariableTable Attribute. The structure is as follows:

     LocalGhostVariableTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 local_ghost_variables_count;
       {
         u2 start_pc;
         u2 start_order;
         u2 end_pc;
         u2 end_order;
         u2 name_index;
         u2 descriptor_index;
         u2 index;
         u2 access_flags;
         u4 BML_flags;
       } local_ghost_variables[local_ghost_variables_count];
     }

The meaning of the fields is as follows:

The initial value of a local ghost variable must be set directly in the code, using a set instruction.

7.7.3 AssertTable Attribute

The AssertTable code attribute represents the table of assertions in the code of the method. The structure of the attribute is as follows:

     AssertTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 asserts_count;
       {
         u2 point_pc;
         u2 index;
         formula_info assertion;
       } asserts[asserts_count];
     }

The meaning of the fields is as follows:

7.7.4 AssumeTable Attribute

The AssumeTable code attribute represents the table of assumptions in the code of the method. The structure of the attribute is as follows:

     AssumeTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 assumes_count;
       {
         u2 point_pc;
         u2 index;
         formula_info assumption;
       } assumes[assumes_count];
     }

The meaning of the fields is as follows:

7.7.5 SetTable Attribute

The SetTable code attribute represent the set instructions to modify ghost fields.

     SetTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 sets_count;
       {
         u2 point_pc;
         u2 order;
         expression_info e1;
         expression_info e2;
       } sets[sets_count];
     }

The meaning of the fields is as follows:

7.7.6 UnreachableTable Attribute

The UnreachableTable attribute represents the table of unreachable points in the code of the method. The structure of the attribute is as follows:

     UnreachableTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 unreachables_count;
       {
         u2 point_pc;
         u2 index;
       } unreachables[unreachables_count];
     }

The meaning of the fields is as follows:

7.7.7 LoopSpecificationTable Attribute

The LoopSpecificationTable attribute represents the table of loop specifications. Its structure is as follows:

     LoopSpecificationTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 loops_count;
       {
         u2 point_pc;
         u2 order;
         formula_info invariant;
         formula_info variant;
       } loops[loops_count];
     }

The meaning of the fields is as follows:

7.7.8 OwnershipTable Attribute

The OwnershipTable code attribute represents the table of ownership modifiers for the types appearing in the code of the method (e.g., associated with any of the instructions new, checkcast, and instanceof). The structure of the attribute is as follows:

     OwnershipTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 ownerships_count;
       {
         u2 point_pc;
         u2 index;
         u4 BML_flags;
       } ownerships[ownerships_count];
     }

The meaning of the fields is as follows:

7.7.9 DebugTable Attribute

The DebugTable code attribute represents the table of debug annotations. Each entry contains one BML expression to be printed out be a BML-aware runtime environment. The structure of the attribute is as follows:

     DebugTable_attribute {
       u2 attribute_name_index;
       u4 attribute_length;
       u2 debug_count;
       {
         u2 point_pc;
         u2 index;
         expression_info expr;
       } debugs[debug_count];
     }

The meaning of the fields is as follows: