6 Outputs

CELIA outputs the following files:

pan-nm.c

contains the C code normalized by Frama-C where each statement has a unique identifier (C comment containing sid). This file contains the full coded needed by the analysis.

pan.eq

contains the inter-procedural control flow graph (ICFG) considered by the analysis. Also, it provides (section penv) the encoding of each function variable into a domain variable.

pan.abs

contains the result of the analysis, i.e., for each statement the number of the file .shp containing the invariant computed by CELIA.

f_XXX.shp

shape files containing the invariants computed by CELIA. To obtain a dot representation of this file please use the program com/shp2dot.sh.

How to read shape files?

A shape file f_XXX.shp is a list of tuples built from

• a shape graph (see CAV'10 publication) which is an abstraction of the heap:
  • the nodes of the graph represent heap sub-lists which are not pointed by pointer program variables; nods are named by n0 (NULL), n1, n2, ... and are labelled by the pointer programs variables which points to the head of the sub-list, and
  • the arcs represent reachability relations (via next field) between sub-lists.
  For example, the shape graph in the invariant intlist-lib-add.c:sid:6 represents a heap with three sub-lists (nodes n1, n2, n3) such that the sub-list stating in n1 is labeled by the program variables x2 and x5 and reaches the sub-list starting in node n2; the sub-list starting in n3 is disjoint from the other sub-lists.
• a list of constraints for each data word abstract domain (in LSUM, MSET, UCONS) used in the analysis.

For the domains LSUM and MSET, the constraints attached to the graph are conjunctions of linear constraints involving the following terms:

xi

represents the value stored in a scalar program variable (see file pan.eq to obtain the variable name),

data(n)

represents the value stored in the head of the sub-list represented by the node n,

len(n)

represents the number of nodes in the sub-list represented by the node n,

sum(n)

represents the sum of values stored in the tail of the sub-list represented by the node n,

mshd(n)

represents the singleton mouldiest containing only the value stored in the first element (head) of the sub-list represented by node n,

mstl(n)

represents the multiset containing the values stored in the tail of the sub-list represented by node n,

For example, the constraint

-mstl(n2)+mstl(n3)=0

in the multi-set constraints in the first shape graph of intlist-lib-add.c:sid:6 says that the multisets of tails of sub-lists represented by nodes n2 and n3 are equal.

For the domain UCONS, the constraints attached to the graph are conjunction structured as follows:

• the econs block are linear constraints on the data(n), len(n) and integer program variables x,
• the following blocks represent universal formulas in the form, e.g.,

  forall y in n. patter-constraint => data-constraint

  which express properties on the data in the sub-lists starting in the node n.

For example, the UCONS constraints in the file intlist-sort-insert:sid:40 contains two universally quantified constraints, both concerning the node n1:

• the first constraint expresses the property that for all cells in the sub-lists n1, represented by y, the data stored in these cells is greater or equal than the data stored in the head of n1, and
• the second constraint expresses the property that for all two cells y1 and y2 in the sub-lists n1 such that y1 <= y2, the data stored in these cells is ordered.