Plugin for Static Analysis and Verification of C Programs with Dynamic Lists

A collection of programs analyzed using CELIA is given below (more examples are in the distribution).

Examples are presented as follows:

WarningSome of the images containing the annotations are very large; please zoom on to have a better displaying.

For example:

Input file intlist-lib-add.c: Normalized code, input of the analysis
(with statement identifiers - sid):
Computed invariants
(indexed by statement identifier):

Summary: intlist-lib-add.c:(sid:6): mset, lsum, ucons,
intlist-lib-add.c:(sid:4): mset, lsum, ucons,
intlist-lib-add.c:(sid:0): mset, lsum, ucons,
intlist-lib-add.c:(sid:3): mset, lsum, ucons,
intlist-lib-add.c:(sid:5): mset, lsum, ucons,
intlist-lib-add.c:(sid:2): mset, lsum, ucons,
intlist-lib-add.c:(sid:1): mset, lsum, ucons,

See also:    APRON    CINV    Frama-C    FIXPOINT    ANR Project Veridyc