Previous: Method Attributes, Up: Encoding of BML in Class File Format
[MH 06032008: attributes for assume, unreachable and debug annotations are missing]
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:
The LocalVariableModifiers attribute represents the BML modifiers of local variables declared in the method code. The structure of the attribute is as follows:
LocalVariableModifiers_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:
ACC_FINAL. All other flags
must be cleared.
BML_NON_NULL, BML_NULLABLE, BML_PEER, BML_REP,
BML_READONLY, BML_ELEM_PEER, BML_ELEM_READONLY.
All other flags must be cleared. Only one of BML_NON_NULL, BML_NULLABLE can be set. Only one
of BML_PEER, BML_REP, BML_READONLY can be set.
Only one of BML_ELEM_PEER, BML_ELEM_READONLY can be set only if
one of BML_PEER, BML_REP, BML_READONLY is set and
the variable is an array.
The format of this table is the closely related to the information contained in the ParameterTable attribute (see Method Attributes). Only local variables which are not parameters can be described here and each one at most once. Parameters can 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 LocalVariableTable JVM attribute (see Methods Data Structure).
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 (Methods Data Structure). The structure is as follows:
LocalGhostVariables_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;
expression_info init_value;
} local_ghost_variables[local_ghost_variables_count];
}
The meaning of the fields is as follows:
CONSTANT_Utf8_info element
CONSTANT_Utf8_info element,
containing a field descriptor encoding the type of a local ghost
variable in the source program
ACC_FINAL. All other flags
must be cleared.
BML_NON_NULL, BML_NULLABLE, BML_PEER, BML_REP,
BML_READONLY, BML_ELEM_PEER, BML_ELEM_READONLY.
All other flags must be cleared. Only one of BML_NON_NULL, BML_NULLABLE can be set. Only one
of BML_PEER, BML_REP, BML_READONLY can be set.
Only one of BML_ELEM_PEER, BML_ELEM_READONLY can be set only if
one of BML_PEER, BML_REP, BML_READONLY is set and
the variable is an array.
The initial value of the local ghost variable must be set directly in the code, using the set instruction.
The Assert code attribute represents the table of assertions in the code of the method. The structure of the attribute is as follows:
Assert_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:
The Assume code attribute represents the table of assumptions in the code of the method. The structure of the attribute is as follows:
Assume_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:
The Set code attribute represent the set instructions to modify ghost fields.
Set_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:
The Unreachable attribute represents the table of unreachable points in the code of the method. The structure of the attribute is as follows:
Unreachable_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:
The LoopSpecification attribute represents the table of loop specifications. Its structure is as follows:
LoopSpecification_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:
The Ownership code attribute represents the table of ownership modifiers
for the types appearing in the code of the method (e.g. after any of the
new
instructions, checkcast, instanceof [JCh 20081312
anything else?]. The structure of the attribute is as follows:
Ownership_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:
BML_PEER, BML_REP,
BML_READONLY, BML_ELEM_PEER, BML_ELEM_READONLY. All other flags must be cleared. Exactly one
of BML_PEER, BML_REP, BML_READONLY must be set.
Only one of BML_ELEM_PEER, BML_ELEM_READONLY can be set,
only if the annotated type is an array type.