The CINV tool provides several abstract domains for abstract reachability analysis of programs manipulating singly linked lists with numerical contents.
The abstract domains of CINV are symbolic representations for specifications which constrain both the shape of the list and the data inside the list. In the present version, three kinds of specifications can be generated: (1) specifications relating data, lenghts, and sums of the data of the list (domain LSUM), (1) specifications relating data, lenghts, and multisets of the data of the list (domain MSET), (2) specifications relating data, lenghts, and universal properties on the elements of the list (domain UCONS).
The input of CINV is a interprocedural control flow graph (ICFG) in the
Fixpoint library
format.
This graph can be obtained from C programs using the
Frama-C plugin
Celia.
Aside the program, CINV has as input the cinv.txt file which fixes its parameters.
The output is the program annotated by specifications given on files with extension .shp.
These files contain a shape value, i.e., a list of constrained heap graphs;
each heap graph is given by tuple built from a graph and a numerical or logical constraint relating the data, the sum of data, and the length of list segments in the graph.
We provide in the following more details on the inputs and output of CINV as well as the presentation of the results obtained when applying CINV on our benchmark.