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