--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on January 2015 ---
On 01/16/2015 03:53 PM, Filip Niksic wrote: > I am trying to verify this using Jessie, as WP cannot deal with dynamic > memory allocation. I am also using libc headers with ACSL specification > that come with Frama-C. I'm afraid that Frama-C headers for functions like malloc are not handled well by the Jessie plugin. Here is your file, slightly modified so as to be processed by Jessie/Why3. The post-condition is not proved, proving it would require significant additional lemmas, stating frame properties about the reachable predicate. For information on those issues in the context of Frama-C, read the following paper. @inproceedings{bobot12icfem, author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre}, title = {Separation Predicates: a Taste of Separation Logic in First-Order Logic}, booktitle = {14th International Conference on Formal Ingineering Methods (ICFEM)}, volume = 7635, series = {Lecture Notes in Computer Science}, publisher = {Springer}, address = {Kyoto, Japan}, month = {November}, year = 2012, abstract = {This paper introduces \emph{separation predicates}, a technique to reuse some ideas from separation logic in the framework of program verification using a traditional first-order logic. The purpose is to benefit from existing specification languages, verification condition generators, and automated theorem provers. Separation predicates are automatically derived from user-defined inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is specified in C/ACSL and verified in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.}, url = {http://proval.lri.fr/publications/bobot12icfem.pdf} } I'm pretty sure that your "reachable" predicate is not convenient for reasoning about linked lists: it should have an additional parameter providing the "list model" of the path from p to q, so as to state properties about disjointness of paths. Additionally to the paper above, you may have a look at the example in Why3 http://toccata.lri.fr/gallery/linked_list_rev.en.html together with the slides/lecture notes at https://www.lri.fr/~marche/MPRI-2-36-1/2014/ Last but not least, if you want to prove C programs involving dynamic data structures, you may consider trying VeriFast : http://people.cs.kuleuven.be/~bart.jacobs/verifast/ Hope this helps, - Claude -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: linked_list.c Type: text/x-csrc Taille: 791 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150119/4771fe1a/attachment.c>