--- layout: fc_discuss_archives title: Message 111 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



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.

> 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.

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.

-Boris