--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2015 ---
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>