2.1 C code

THIS PART IS OBSOLTE SINCE REPLACED BY THE CELIA PLUGIN. PLEASE CONSULT CELIA DOCUMENTATION.

Each example is given as a C function. The function has at least one list parameter of type intlist or its is the main function. The C definition of type intlist corresponds to a singly linked list with an integer data field as follows:

typedef struct intlist_ * intlist;
struct intlist_ {
  int data;
  intlist next;
};

The C code used is a very simple subset of C including pointers. In this code, all the statements shall be elementary. For instance, composed terms (e.g., x->next->data) and statements (e.g., x=y with x not pointing to NULL) are not elementary.

The C functions are specified using the logic presented in Specification logic.