FFX (Flow Fact in XML) format
A. Bonenfant , H. Cassé , M. De Michiel

Content

13 Data Flow Constraints

The data constraints provides a rich way to give information about the data flow between different data. In the opposite of data properties, they provide an axiomatic representation of the program properties. As for the data properties, they applies to the whole scope of the control flow element containing them but they uses the same syntax to locate a particular global or local variable.

The DATA-CONSTRAINT element is defined below. They may be either a data relation or composed of AND and OR operators: 

DATA-CONSTRAINT ::=
  | DATA-RELATION
  | <not> DATA-CONSTRAINT </not>
  | <and> DATA-CONSTRAINT+ </and>
  | <or> DATA-CONSTRAINT+ </or>

The DATA relation is defined below: 

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>

The relation between two data expression may be equality – eq, inequality – ne, less than – lt, less or equal – le, greater than – gt or greater or equal – ge.

Finally, the data expression is made of: 

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>

The data expression allows to cover the usual set of operations available in the programming languages, that is: