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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 82, Issue 1



Hi,

I did an attempt to prove a cycle detection function a long time ago

https://github.com/nicolasmarti/mylibc

only one subgoal cannot be proved, as integer is not accepted for ghost
variables

regards
Nicolas
On Mar 10, 2015 8:00 PM, <frama-c-discuss-request at lists.gforge.inria.fr>
wrote:

> 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. Verification of linked list (Wenrui Meng)
>    2. Re: Verification of linked list (David MENTRE)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 10 Mar 2015 00:05:29 -0400
> From: Wenrui Meng <wenrui at seas.upenn.edu>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: [Frama-c-discuss] Verification of linked list
> Message-ID:
>         <
> CAF08Yjs_djVFrVxyvkgigYEW_ZaeuEYBttqsNEmG1_3iOvUNJA at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Dear All,
>
> In the ASCL tutorial, there is a example about linked list. Does frama-c
> support its verification? I copied the example but frama-c cannot verify
> it. What shall I do to enable frama-c to prove it? Add loop invariant?
>
> I didn't find much related examples resource for beginner. Can any one
> point out examples by WP plug?
>
> Thanks,
> Wenrui
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150310/2273f0b3/attachment-0001.html
> >
>
> ------------------------------
>
> Message: 2
> Date: Tue, 10 Mar 2015 08:43:02 +0100
> From: David MENTRE <dmentre at linux-france.org>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] Verification of linked list
> Message-ID: <54FEA086.7090800 at linux-france.org>
> Content-Type: text/plain; charset=windows-1252; format=flowed
>
> Hello,
>
> Le 10/03/2015 05:05, Wenrui Meng a ?crit :
> > I didn't find much related examples resource for beginner. Can any one
> > point out examples by WP plug?
>
> You should take a look at "ACSL by Example" from Fraunhofer FOKUS:
>
>
> https://www.google.fr/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&ved=0CC0QFjAB&url=https%3A%2F%2Fwww.fokus.fraunhofer.de%2Fdownload%2Facsl_by_example&ei=4J_-VPbCLcflUo-0gZAM&usg=AFQjCNHMBZrnDJrrTeo-_Dc9LNMKzLfyfg&bvm=bv.87611401,d.d24&cad=rja
>
> Best regards,
> david
>
> PS @Jens: finding the PDF file is always difficult. ;-) You should put
> it on a simple web page or attached to a blog entry.
>
>
>
> ------------------------------
>
> 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 82, Issue 1
> **********************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150311/6a6491ba/attachment.html>