--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on January 2015 ---
[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>