4 Inputs

CELIA plug-in shall receive as inputs the list of C files containing:

• the C function to be analyzed called the entry point of the analysis (by default main) and
• all the C functions called by the entry point.

The C functions that can be analyzed with CELIA shall satisfy the following constraints:

• they shall use only variables of type int and intlist (the last defined in the file intlist.h),
• the assignment statements for pointer variables shall be elementary, i.e., a pointer can be assigned only if it is NULL, only the pointer left values x, x->data, and x->next are allowed,

  This limitation will be removed in future versions of CELIA.

• the conditions on pointer variables shall also be elementary, i.e., only terms x and x->data are allowed,

  This limitation will be removed in future versions of CELIA.

• the Boolean conditions used in if andwhile statements shall be atomic,

  This limitation will be removed in future versions of CELIA.

• the actual parameters in function calls shall be variables,

  This limitation will be removed in future versions of CELIA.

• the output actual parameters in function calls shall be pointers to lists.

The C file in input of CELIA can be annotated with specifications in the ACSL logic of Frama-C. The file intlist.h defines several predicates that can be used in these annotations. Currently, only these predicates are considered by CELIA. Also, only annotations corresponding to function pre-conditions are interpreted. The semantics of these predicates is explained here.