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] Non-terminating loops
- Subject: [Frama-c-discuss] Non-terminating loops
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Fri, 28 May 2010 14:39:03 +0200
- In-reply-to: <1275049412.2159.26.camel@iti27>
- References: <1274979944.3488.36.camel@iti27> <4BFED922.9080101@inria.fr> <1275049412.2159.26.camel@iti27>
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
- References:
- [Frama-c-discuss] Non-terminating loops
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Non-terminating loops
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Non-terminating loops
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Non-terminating loops
- Prev by Date: [Frama-c-discuss] Unknows Pragma
- Next by Date: [Frama-c-discuss] Non-terminating loops
- Previous by thread: [Frama-c-discuss] Non-terminating loops
- Next by thread: [Frama-c-discuss] Non-terminating loops
- Index(es):