CELIA has been applied to:
- static analysis and assertion inference for C programs using lists with integer data
- verification of assertions for C programs with lists
Examples are presented as follows:
- the input C file (see the syntactic limitations in the documentation),
- the C file containing the code of all functions called in the initial C file and the code normalized by Frama-C with a unique identifier (sid) for each statement,
- the result of the analysis/verification is presented as a table of assertions/verification results indexed by the statement identifier (sid),
Some of the images containing the annotations are very large; please zoom on to have a better displaying.