Previous: Method Attributes, Up: Encoding of BML in Class File Format
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 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:
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 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.
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:
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 a local ghost variable must be set directly in the code, using a set instruction.
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:
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:
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:
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:
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:
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:
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.
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: