FFX (Flow Fact in XML) format
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
8 Loop Bound Attributes
Loop bound attributes are of INFORMATION-ATTRIBUTE but are limited to the loop elements.
LOOP-ATTR ::= | maxcount="INT|NOCOMP"? | mincount="INT|NOCOMP"? | totalcount="INT|NOCOMP"? | exact="BOOL"? | executed="BOOL"? | expmaxcount="TEXT"? | exptotalcount="TEXT"?
| Attribute | Description |
|---|---|
| maxcount | the maximum number of time the loop iterates after each entry |
| totalcount | the maximum number of time the loop iterates for the whole program run |
| exact | true if the totalcount is exact or false if it is overestimated |
| executed | false if the loop is never executed, true if the loop executes in some cases |
| expmaxcount | maxcount as a formula (if NOCOMP) |
| exptotalcount | totalcount as a formula (if NOCOMP) |
The last two attributes define the count as a formula with the given syntax:
expression ::=
INT
| '-' expression
| '(' expression ')'
| expression '+' expression
| expression '-' expression
| expression '*' expression
| expression '/' expression