Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Dynamically allocated lists


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>