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
15 Appendix A: FFX Grammar
<!-- top level elements --> FLOWFACTS ::= <flowfacts> TOP-LEVEL-ITEM* </flowfacts> TOP-LEVEL-ITEM ::= CONTEXT | FUNCTION | DATA | CONTROL CONTEXT ::= <context name="TEXT"> TOP-LEVEL-ITEM* </context> FUNCTION ::= <function LOCATION-ATTRS INFORMATION-ATTRS> STATEMENT* </function> <!-- statements --> STATEMENT ::= | BLOCK | LOOP | CALL | CONDITIONAL | DATA | DATA-CONSTRAINTS | CONTROL-CONSTRAINTS BLOCK ::= <block LOCATION-ATTRS INFORMATION-ATTRS/> LOOP ::= <loop LOCATION-ATTRS INFORMATION-ATTRS> STATEMENT* </loop> | <loop LOCATION-ATTRS INFORMATION-ATTRS> <iteration number="INT"> STATEMENT* </iteration> </loop> CALL ::= <call LOCATION-ATTRS INFORMATION-ATTRS> FUNCTION+ </call> CONDITIONAL ::= <conditional CONDITIONAL-ATTRS LOCATION-ATTRS> CONDITION? CASE+ </conditional> CONDITIONAL-ATTRS ::= | expcond=”TEXT” | precision=”EXACT|MAX|NOCOMP” CONDITION ::= <condition CONDITION-ATTRS LOCATION-ATTRS> CONDITIONAL | STATEMENT STATEMENT* </condition> CASE ::= <case CASE-ATTRS LOCATION-ATTRS> CONDITIONAL | STMT </case> CASE-ATTRS ::= | cond="INT" | count="INT | NOCOMP" | expcount="TEXT" <!-- data definition --> DATA ::= <data ID-ATTRS DATA-ATTRS > ID-ELEMENTS DATA-PROPERTY* </data> ID-ATTRS ::= | address = "ADDR" | name = "TEXT" | name = "TEXT" offset = "INT" | offset = "INT" | name = "TEXT" local = "yes" ID-ELEMENT ::= <ref> REF-ELEMENT </ref> REF-ELEMENT ::= | <mem> REF-ELEMENT </mem> | <field of="name"/> | <item> DATA-EXPR </item> | <range> DATA-EXPR DATA-EXPR </range> | <all> <!-- location attributes --> LOCATION-ATTRS ::= | IDENTIFICATION | ADDRESS-LOCATION | LABEL-LOCATION | SOURCE-LOCATION IDENTIFICATION ::= id = "TEXT" ADDRESS-LOCATION ::= <element address="INT"/> LABEL-LOCATION ::= | <element label="TEXT"/> | <element label="TEXT" offset="INT"/> | <element offset="INT"/> SOURCE-LOCATION ::= | <element source="TEXT" line="INT"/> | <element line="INT"/> <!-- loop bound attributes --> LOOP-ATTR ::= | maxcount="INT|NOCOMP"? | mincount="INT|NOCOMP"? | totalcount="INT|NOCOMP"? | exact="BOOL"? | executed="BOOL"? | expmaxcount="TEXT"? | exptotalcount="TEXT"? expression ::= INT | '-' expression | '(' expression ')' | expression '+' expression | expression '-' expression | expression '*' expression | expression '/' expression <!-- execution attributes --> TIME-EXECUTION-ATTR ::= | maxtime="INT"? | time="INT"? | mintime="INT"? | freq="INT"? | maxfreq="INT"? | minfreq="INT"? <!-- control flow properties --> CONTROL-PROPERTIES ::= | <no-return LOCATION-ATTRS/> | <no-call LOCATION-ATTRS/> | <ignore-entry name="TEXT"/> | <return LOCATION-ATTRS/> | <multibranch LOCATION-ATTRS> <target LOCATION-ATTRS />* </multibranch> | <multicall LOCATION-ATTRS> <target LOCATION-ATTRS /> </multicall> <!-- control flow constraints --> CONTROL-CONSTRAINT ::= <control-constraint> CONTROL-PREDICATE </control-constraint> CONTROL-PREDICATE ::= | CONTROL-RELATION | <and> CONTROL-RELATION+ </and> | <or> CONTROL-RELATION+ </or> CONTROL-RELATION ::= | <eq> CONTROL-FORMULA CONTROL-FORMULA </eq> | <ne> CONTROL-FORMULA CONTROL-FORMULA </ne> | <lt> CONTROL-FORMULA CONTROL-FORMULA </lt> | <le> CONTROL-FORMULA CONTROL-FORMULA </le> | <gt> CONTROL-FORMULA CONTROL-FORMULA </gt> | <ge> CONTROL-FORMULA CONTROL-FORMULA </ge> CONTROL-FORMULA ::= | <int>INT</int> | <count ref="TEXT"/> | <neg> CONTROL-FORMULA </neg> | <add> CONTROL-FORMULA CONTROL-FORMULA </add> | <sub> CONTROL-FORMULA CONTROL-FORMULA </sub> | <mul> CONTROL-FORMULA CONTROL-FORMULA </mul> | <div> CONTROL-FORMULA CONTROL-FORMULA </div> <!-- data flow properties --> DOMAIN-PROPERTY ::= | SCALAR-DOMAIN | POINTER-DOMAIN | ARRAY-DOMAIN | STRUCT-DOMAIN SCALAR-PROPERTY ::= | <const value="VALUE"/> | <range lower="VALUE"? upper="VALUE"? step="INT"?/> POINTER-PROPERTY ::= | <address> ADDR </address> | ID-ELEMENT ARRAY-DOMAIN ::= <array> ARRAY-ITEM* </array> ARRAY-ITEM ::= | <item index="INT"> DOMAIN-PROPERTY </item> | <range lower="INT" upper="INT"> DOMAIN-PROPERTY </range> | <other> DOMAIN-PROPERTY </other> STRUCT-DOMAIN ::= <struct> STRUCT-FIELD* </struct> STRUCT-ITEM ::= <field name="TEXT"> DOMAIN-PROPERTY </field> MUTABILITY-PROPERTY ::= <mutable kind="MUTABILITY-KIND"/> MUTABILITY-KIND ::= no | out | in <!-- data flow constraints --> DATA-CONSTRAINT ::= | DATA-RELATION | <not> DATA-CONSTRAINT </not> | <and> DATA-CONSTRAINT+ </and> | <or> DATA-CONSTRAINT+ </or> DATA-RELATION ::= | <eq>DATA-EXPR DATA-EXPR</eq> | <ne>DATA-EXPR DATA-EXPR</ne> | <lt>DATA-EXPR DATA-EXPR</lt> | <le>DATA-EXPR DATA-EXPR</le> | <gt>DATA-EXPR DATA-EXPR</gt> | <ge>DATA-EXPR DATA-EXPR</ge> DATA-EXPR ::= | <true/> | <false/> | <int>INT</int> | <float>FLOAT</float> | <enum>TEXT</enum> | <var ID-ATTRS> ID-ELEMENTS? </var> | <neg> DATA-EXPR </neg> | <inv> DATA-EXPR </inv> | <add> DATA-EXPR DATA-EXPR </add> | <sub> DATA-EXPR DATA-EXPR </sub> | <mul> DATA-EXPR DATA-EXPR </mul> | <div> DATA-EXPR DATA-EXPR </div> | <mod> DATA-EXPR DATA-EXPR </mod> | <shl> DATA-EXPR DATA-EXPR </shl> | <shr> DATA-EXPR DATA-EXPR </shr> | <bin-and> DATA-EXPR DATA-EXPR </bin-and> | <bin-or> DATA-EXPR DATA-EXPR </bin-or> | <bin-xor> DATA-EXPR DATA-EXPR </bin-xor>