2.1.1.1 First not null

C code 
Spl encoding

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
intlist fstNot0(intlist x) {
  intlist xi = x;
  while (xi != NULL && xi->data==0) {
    xi = xi->next;
  }
  return xi;
}


var _data:real, _free:real, _len:real, 
    _new:real, _next:real, _null:real,
    x:real, xi:real, y:real, yi:real,
    _l:int, _k:int, S:int;
begin
  assume (x == 0); 
  xi = _null; y = _null; 
  xi = x;
  while xi != _null and (xi* _data == 0) do
    y = xi*_next;
    xi = _null;
    xi = y;
    y = _null;
  done;
end

Results

Domain 
Param. 
Log file 
Interesting constraint

LSUM-PRD
Anon=(0,1)
log/intlist-fstNot0-lsum-prd-01
x(n1) and xi(n2) and d(n1)=0
and S(n1)=0 and d(n2)+S(n2)=S
and _l=l[n1]+l[n2]


LSUM-REL
Anon=(0,1)
log/intlist-fstNot0-lsum-rel-01
same as above


MSET
TODO
TODO
x(n1) and xi(n2) and d(n1)=0
and M[n1]=\0\ and M[n1]+M[n2]=M
and _l=l[n1]+l[n2]


UCONS
Anon=(0,1), P11
TODO
x(n1) and xi(n2) and d(n1)=0
and \forall y \in n1 \implies d(y)=0

Because the numerical domain used now (polygons) is not able to represent the inequality constraints, the invariant obtained at the control point corresponding to the end of the loop does not contain the constraint xi->data!=0.