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