--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 84, Issue 15



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>