Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] issues with the ACSL Post label
- Subject: [Frama-c-discuss] issues with the ACSL Post label
- From: x_cui at hotmail.com (Xiao-lei Cui)
- Date: Sun, 1 Dec 2013 20:44:17 -0500
- In-reply-to: <CAEt_dErdeRPm0FQon35=E=vx8Od6w-cXXeASxv8B+4P52tM0ag@mail.gmail.com>
- References: <BAY169-W791B99FF16C894E692A16C97E90@phx.gbl>, <CAA1cxuhbHXpRvQbopVBNsqNGzVKGAUS1j=xSK-kBr51ggF5nLQ@mail.gmail.com>, <CAEt_dEoZSi6Dgak2Upo4NyaziBRnJmB=LXHTfxaSd0iRni4gKQ@mail.gmail.com>, <CAEt_dErdeRPm0FQon35=E=vx8Od6w-cXXeASxv8B+4P52tM0ag@mail.gmail.com>
Hi, Thanks for the helpful comments! I will try to avoid the usage of "Post" label in the ensure clause. Just for the knowledge of ACSL, is it safe to say that in the ensures clause the "Post" label is implicitly assumed to refer post state? And "Here" label in the ensures clause actually refer to the post state as well? for instance, suppose I would specify a function of which post state is a==0 : ensures a==0; <==> ensures \at(a, Here)==0; /* "Here" refers to the state after function execution?*/ <==> ensures \at(a, Post)==0; thanks.. cheers, xiao-lei To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] issues with the ACSL Post label Perhaps I should've been more explicit: Here is equivalent to Pre This is not true. the Here label refers to the state in which the annotation is evaluated. eg: when used with requires, it refers to the pre-state, when used in ensure it refers to the post-state, when used in loop invariants it refers to the current iteration. Omitting the \at clause or using \at( _ , Here) is equivalent, as such: *a == \at(*a, Here) will always hold By removing the 'Post' label from above annotation, the VCs can be generated and proved. Like I said before, omitting the \at clause is equivalent to \at(*a, Here) Pre is equivalent to Old ? Yes, \old(*a) == \at(*a, Pre) -- Cumprimentos,Cristiano Sousa _______________________________________________ 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131201/6cd643dd/attachment.html>
- Prev by Date: [Frama-c-discuss] Is there any plan for the new release of frama-c?
- Next by Date: [Frama-c-discuss] problem with \strlen and \offset constructs
- Previous by thread: [Frama-c-discuss] Is there any plan for the new release of frama-c?
- Next by thread: [Frama-c-discuss] problem with \strlen and \offset constructs