--- layout: fc_discuss_archives title: Message 114 from Frama-C-discuss on May 2010 ---
Boris Hollas wrote: > Hello Claude, > > >> 1) in Beryllium-2 and Why 2.21, the pragma JessieTerminationPolicy is >> not available yet >> > > It seems it is, because Pascal's example works for me. > > I guess it is because Jessie/Why 2.21 ignores the pragma (there should be a warning) and before version 2.23, the behavior corresponding to JessieTerminationPolicy(user) was the default. the default to *always* generate a VC for termination was decided because some user requested that a program with all VCs should be totally correct, that is the default should the more strict notion of correctness. >> 3) terminates clause is not supported by Jessie even in the most recent >> version. This is documented and if you look carefully you should see a >> warning. >> > > In both the acsl-beryllium2 and the acsl-boron documentation terminates > is marked as "Experimental" in section "2.5.4 Non-terminating > functions". If it is not supported yet, it should be indicated. I > understand "Experimental" as something that has been implemented, but > may not work in all circumstances. > "terminates" clauses are perfectly well supported... by the Frama-C kernel. Jessie is just one of the Frama-C plugins, and may not support everything, and what is supported or non supported is given in the appendix of Jessie's manual. > If pragma JessieTerminationPolicy is implemented in Boron, it should be > mentionen in section "2.5.4 Non-terminating functions" of the acsl-boron > documentation. So far, it is only mentioned in the Jessie-tutorial. > Since it is a Jessie-specific pragma, there is no reason why it should appear in the ACSL-Boron doc. -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |