--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on July 2010 ---
[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>