--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on May 2015 ---
Thank you Mr. Prevosto! 2015-05-30 7:00 GMT-03:00 <frama-c-discuss-request at lists.gforge.inria.fr>: > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. Frama-C ACSL examples (V?tor Alcantara de Almeida) > 2. Re: Frama-C ACSL examples (Virgile Prevosto) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 29 May 2015 11:10:55 -0300 > From: V?tor Alcantara de Almeida <vitoralcantara at ppgsc.ufrn.br> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: [Frama-c-discuss] Frama-C ACSL examples > Message-ID: > < > CAJ9RV_M6wedaON1P6xnTo+9OYkKuYUbktTaOvzNO38BoY1CvOQ at mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Dear Frama-C users and developers, > > I'm developing a plugin for Frama-C and, to test it, I'm using some > examples found in "ACSL by Example" and the Jessie plugin. So I come to ask > if someone has available examples of annotated C code or could inform > where I can find them, specially examples that weren't successfully proved. > > Thank you in advance, > V?tor Alc?ntara de Almeida > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150529/e04cdc2f/attachment-0001.html > > > > ------------------------------ > > Message: 2 > Date: Fri, 29 May 2015 18:37:07 +0200 > From: Virgile Prevosto <virgile.prevosto at m4x.org> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Subject: Re: [Frama-c-discuss] Frama-C ACSL examples > Message-ID: > <CA+yPOVhruvtxg0K0S2eHRHws3ufrBFcWmmCMQivocr= > CZdB0_w at mail.gmail.com> > Content-Type: text/plain; charset=UTF-8 > > Hello, > > 2015-05-29 16:10 GMT+02:00 V?tor Alcantara de Almeida > <vitoralcantara at ppgsc.ufrn.br>: > > someone has available examples of annotated C code or could inform > where I > > can find them, specially examples that weren't successfully proved. > > > > - The wiki contains material from various tutorials > https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial. > A certain number of them have code examples with ACSL specifications > to be validated by WP. > - The Toccata team from Inria maintains a gallery of verified > programs, including some verified with Frama-C: > http://toccata.lri.fr/gallery/frama-c.en.html > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > ------------------------------ > > End of Frama-c-discuss Digest, Vol 84, Issue 15 > *********************************************** > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150530/70fc565e/attachment.html>