Content
- 1 Introduction
- 2 Notation
- 3 Tool Usage
- 4 Top Level Elements
- 5 Control Flow Elements
- 6 Data Flow Elements
- 7 Location Attributes
- 8 Loop Bound Attributes
- 9 Time and Execution Attributes
- 10 Control Flow Properties
- 11 Control Flow Constraints
- 12 Data Flow Properties
- 13 Data Flow Constraints
- 14 Future Developments
- 15 Appendix A: FFX Grammar
- 16 Appendix B: Example – output of oRange tool
7 Location Attributes
Location attributes allows to identify code either from the binary, or from the sources. This is performed using different sets of attributes according to the used method.
LOCATION-ATTRS ::= | IDENTIFICATION | ADDRESS-LOCATION | LABEL-LOCATION | SOURCE-LOCATION
7.1 Identification
The IDENTIFICATION is not really a location in the program representation but allows to make a reference to part a part of code represented by the other location attributes. For example, it is used in a control constraint to identify the count of executions of a code part.
IDENTIFICATION ::= id = "TEXT"
7.2 Address Location
The address location is the most simple scheme. A simple attribute gives the address but one may notice that this location kind may be invalidated each time the application is compiled.
ADDRESS-LOCATION ::= <element address="INT"/>
7.3 Label Location
The label location provides more flexibility. It encode location either by a label, or by a label and an offset. This scheme does not support re-compilation but linkage of a library because, as the code is not modified, cause only the translatation of the label address from one position to another one.
LABEL-LOCATION ::= | <element label="TEXT"/> | <element label="TEXT" offset="INT"/> | <element offset="INT"/>
One may observe there a three forms:
only label computes the address of the label
label and offset computes the sum of the label address and offset
only offset computes the sum of the closer embedding label definition and of the offset.
The last form allows to reduce verbosity as most offsets are relative to the function that contains them.
7.4 Source Location
Source location supports re-compilation, linking but not source modification. It defines the location as a source file name and a line in this file. To work, it requires to work either on sources, or on binary embedding debugging information.
SOURCE-LOCATION ::= | <element source="TEXT" line="INT"/> | <element line="INT"/>
The second form allow to re-use source attribute value of the closer embedding element.