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] how to deal with malloc in frama-c (boron)

Le ven. 30 juil. 2010 11:12:30 CEST,
Alwyn Goodloe <agoodloe at gmail.com> a ?crit :

> It would be great if the examples in examples-c were updated for jessie. It
> might cut down on a lot of
> questions about how to annotate  programs.  For instance, the parray.c code
> is just the sort of thing
> that the jessie/ACSL tutorials don't seem to show and I'm not sure where to
> look other than these examples,
> which aren't correct so they don't really help.
> 

As a matter of fact, I've adapted parray.c to ACSL after Nicolas'
e-mail. FWIW, the result is attached to this mail. It typechecks with
Frama-C, but at the moment it suffers from the lack of support for
\fresh in Jessie Nicolas complained about.

-- 
E tutto per oggi, a la prossima volta.
Virgile

-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: parray_frama_c.c
Type: text/x-c++src
Taille: 3407 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100730/c9ee7496/attachment.cc>