--- layout: fc_discuss_archives title: Message 107 from Frama-C-discuss on October 2008 ---
Hi, I do not mean to alter in any way what was decided for ACSL. I am just saying that the Jessie plugin default is to generate termination VC only for those loops annotated with variants. I recall that the Jessie plugin is not ACSL! Yannick On Thu, Oct 23, 2008 at 2:55 PM, Pascal Cuoq <Pascal.Cuoq@cea.fr> wrote: > > On Oct 23, 2008, at 2:28 PM, Yannick Moy wrote: > >> It is still to be decided whether we define an option to force >> termination checking, or if this should be the default, with an option to >> switch back to the current behavior. >> > > Actually, I think that it has been decided that a clause "terminates p;" > can be part of a function contract in ACSL, and that a function is > acceptable > with respect to such a contract as long as it terminates every time > p is true in its pre-state (keeping in mind that the pre-condition is > supposed to hold in the pre-state too, so that the function does not > have to terminate if p holds but the pre-condition doesn't). > > Partial correctness results can be expressed by adding > a "terminates false;" clause to the contract every function in the program. > It would be bad style if the meaning of contracts > changed according to command-line options. > > Further explanations and examples are provided in section 2.5 > of version 1.3 of the ACSL document, which reflects what was > agreed on by the ACSL committee as far as I remember. > > Pascal > > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081023/4730322c/attachment.htm