Next: Examples by class, Previous: Copying, Up: Top
The CINV tool provides several abstract domains for abstract reachability analysis of programs manipulating singly linked lists with numerical contents.
CINV generates for each control point specifications which constrain both the shape of the list and the data inside the list. In the present version, two kinds of specifications can be generated: (1) specifications relating data, lenghts, and sums of the data of the list and (2) specifications relating lenghts, data, and universal properties on the list segments.
The input of CINV is an SPL program containing an initial condition on the lists used by the program. Another input of CINV is the cinv.txt file giving the maximum number of simple nodes on the heap graph.
The output is the program annotated by program specifications given on files with extension .shp.
These files contain a list of constrained heap graphs, i.e., in constraint is given in the form of 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.