A collection of programs analyzed using CELIA is given below (more examples are in the distribution).
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 annotations synthesized with each abstract domain for each program point (see the documentation for how to read these annotations); the summaries synthesized for each function called are displayed in red!
Some 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, |
-
A basic library of singly linked lists:
- intlist.h (header file for type & predicates definition)
- intlist-lib-add.c (add an integer at the begining of the list)
- intlist-lib-add_tail.c (add an integer at the end of the list, iterative version)
- intlist-lib-add_tail_rec.c (add an integer at the end of the list, recursive version)
- intlist-lib-del.c (delete the first element of the list)
- intlist-lib-del_tail.c (delete the last element of the list, iterative version)
- intlist-lib-del_tail_rec.c (delete the last element of the list, recursive version)
- intlist-lib-empty.c (test if the list is empty)
- intlist-lib-init.c (create a list of a given length)
- intlist-lib-printlist.c (print a list)
-
Traversals of one or two singly linked lists (aka map and map2):
- intlist-map-addV.c (add some value to each element)
- intlist-map-initFibo.c (initialization with Fibonacci sequence)
- intlist-map-initSeq.c (initialization in sequence starting from a value)
- intlist-map-initSeqEven.c (initialization with sequence of even numbers)
- intlist-map-initV.c (initialization with a given value)
- intlist-map2-add2_eq.c (copying data by adding 2)
- intlist-map2-addV_eq.c (copying data by adding some value in parameter)
- intlist-map2-copy_rec.c (copying data between lists of different length, recursive version)
-
Accumulation of results from one or two singly linked lists (aka fold and fold2):
- intlist-fold-clone.c (copy a list)
- intlist-fold-copyGe5.c (collect a copy of all elements with data greater than 5)
- intlist-fold-copyGeV_rec.c (like above, constant given as parameter and recursive version)
- intlist-fold-max.c (compute max element)
- intlist-fold-reverse.c (reverse a list)
- intlist-fold-split_rec.c (dispatch copies into two equilibrated lists, recursive version)
- intlist-fold-splitV.c (dispatch using some value)
- intlist-fold-sum.c (computes the sum)
- intlist-fold2-concat.c (copy-concatenates two lists)
- intlist-fold2-equal.c (test equality of two lists)
- intlist-fold2-merge.c (merge two lists)
- Sorting algorithms:
-
GTK library for singly linked lists:
- gslist.h (general definitions, adaptation of the original version)
- gslist.c (full implementation, adaptation of the original version)