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



Boris Hollas wrote:
> 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.
>
>   
I guess it is because Jessie/Why 2.21 ignores the pragma (there should 
be a warning) and before version 2.23,
the behavior corresponding to JessieTerminationPolicy(user) was the default.

the default to *always* generate a VC for termination was decided 
because some user requested that a program
with all VCs should be totally correct, that is the default should the 
more strict notion of correctness.

>> 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.
>   
"terminates" clauses are perfectly well supported... by the Frama-C kernel.

Jessie is just one of the Frama-C plugins, and may not support 
everything, and what is supported
or non supported is given in the appendix of Jessie's manual.

> 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.
>   
Since it is a Jessie-specific pragma, there is no reason why it should 
appear
in the ACSL-Boron doc.


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |