--- layout: fc_discuss_archives title: Message 113 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Non-terminating loops



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