2.0.2 Spl encoding

The Spl language is the input language of the Interproc tool Jeannet. Since Spl deals only with numeric (integer or real) variables, we encode our programs on lists as follows:

• Variables of type intlist are coded by real variables.
• Data variables are encoded by integer variables. By convention, length variables are the first two integer variables. (This is a constant fixed in the code.) The other integer variables are considered data variables. This separation of length and data variables is used only by the domains which deal differently with these variables, e.g., the LSUM-PRD domain LSUM-PRD.
• The following real variables shall be present in any Spl encoding program in the first positions of the declaration list for real variables: _data, _free, _len, _new, _next, and _null. They are used to encode operations on list variables, e.g., the data field access for a list variable x, x->data, is encoded by the expression x*_data. Similarly, the _next variable is used to encode the next field access. The _free (resp. _new) variable is used to encode the free (resp. new) statement for the memory deallocation (resp. allocation) of pointers. The _len variable cannot be used for the moment. The _null variable encodes the predefined NULL constant in C.
• All statements are elementary, i.e., the only terms used on pointer variables are x, x->data, and x->next, and the statements have as left hand side one of the terms above and when terms x and x->next are assigned, they have to be NULL.
• Since Spl considers only numerical variables, the left hand side of an assignment shall be a variable. Or, to assign fields of list variables we need left hand sides of assignments to be expressions, e.g., x->data encoded by x*_data. To encode such assignments we use the divisibility operation on reals, i.e., x->field=expr is encode by x=expr/field.
• The specification properties (see Specification logic) of the code is encoded into an initial assume statement of the form assume(x==<code>); with the following semantics:

  x==0

  acyclic(x) and l[x]=_l and data(x), e.g. data(x)=`S[x]=S'
  

  x==1

  acyclic(x) and l[x]+l[y]=_l and _l>=1 and data(x,y) and reach(x,y), e.g., data(x,y)=`S[x]+S[y]=S'
  

  x==2

  acyclic(x) and l[x]=_l and data(x) and acyclic(y) and l[y]=_l and data(y) and _l>=1 and disjoint(x,y)
  

  x==3

  acyclic(x) and l[x]=_l and data(x) and acyclic(y) and l[y]+1<=_l and data(y) and _l>=1 and disjoint(x,y)
  

  x==4

  acyclic(x) and l[x]=_l and data(x) and acyclic(y) and l[y]=_l and data(y) and acyclic(z) and l[z]=_l and data(z) and _l>= 1 and disjoint(x,y,z)