7.5.2 LocalGhostVariables Attribute

This attribute describes the local ghost variables defined in the code. The structure of the attribute data and the meaning of the fields is very similar to The LocalVariableTable attribute. The structure is the following:

     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;
         expression init_value;
       } local_ghost_variables[local_ghost_variables_count];
     }

JCh: [FIXME] annotations?

The meaning of the fields is the following:

• attribute_name_index - index in the constant pool of the attribute name (org.bmlspecs.LocalGhostVariables)
• attribute_length - length in bytes of the whole structure
• local_ghost_variables_count - the number of local ghost variables in the table
• local_ghost_variables - the table of local ghost variables; the fields in each element of the array have the following meaning:
  • start_pc - start of the code fragment, where the given local ghost variable has a meaningful value
  • start_order - the position of the variable declaration in BML declarations at code address start_pc
  • end_pc - end of the code fragment, where the given local ghost variable has a meaningful value; the variable has a meaningful value strictly before this point
  • end_order - the position of the end of the variable scope in BML declarations at code address end_pc
  • name_index - the index in the second constant pool where the variable name is stored as a CONSTANT_Utf8_info element
  • descriptor_index - the index in the second constant pool where the variable type is stored as a CONSTANT_Utf8_info element, containing a field descriptor encoding the type of a local ghost variable in the source program
  • index - local variable index by which this variable is referenced in BML expressions appearing in this method
  • init_value - optional initial value of the field JCh: [FIXME] is it needed? Or we can assume it is encoded by a set instruction in a start_pc position? [for Java local variables - bytecode instructions are generated to initialize the variable and there is no place for init_value anywhere in the .class file