--- layout: fc_discuss_archives title: Message 113 from Frama-C-discuss on May 2010 ---
Le ven. 28 mai 2010 14:23:32 CEST, Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit : > > 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 In the acsl-boron implementation notes, implemented refers to ACSL constructions that are supported by Frama-C's kernel, which essentially means that such specifications will be parsed and type-checked by Frama-C. It does not say anything about what a particular plug-in will do about it (to be honest, I don't think that any plug-in does something sensible with terminates clause at the moment, but please remember that the Jessie plug-in is only a component of Frama-C, albeit an important one). > 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. Well, this concerns Jessie-specific constructions, so it seems to me that Jessie documentation is the appropriate place to mention it. Best regards, -- E tutto per oggi, a la prossima volta. Virgile