--- layout: fc_discuss_archives title: Message 117 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:
> On Fri, 2010-05-28 at 14:42 +0200, Claude Marche wrote:
>   
>> "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
>>     
>
> It doesn't much help me that I know that some ACSL keywords are parsed
> by the Frama-C kernel if I want to verify code. 
Sorry about that. But still I think we need to insist on the distinction 
between Frama-C/ACSL on one side,
and Jessie which is just one of the plugin among dozens of others.
> I'd much appreciate a
> manual that documents which ACSL keywords are implemented in Jessie +
> why and which ones aren't. 
Jessie manual should give you that...
> For example, the Jessie tutorial
> http://frama-c.com/jessie/jessie-tutorial.pdf lists abrupt termination
> clauses in "7.2.3 Unsupported ACSL features", but no termination
> clauses. Obviously, I can't conclude that termination clauses are
> supported by Jessie. 
.. although you're right that the current version on the web is 
outdated. This will be fixed soon.

> The same is true for C constants (as in const int
> n=10;), see "7.2.1 Unsupported C features". 
Ah yes, that question about consts... It deserves an answer in the 
corresponding thread.
> I used to do experiments
> with test code to discover what features are implemented in Jessie, but
> this just takes too much time.
>   
Sorry about that. I'm also losing a lot of time to maintain Jessie 
source code and documentation, to do my best to answer to the mails of 
the public list in a hopefully useful and constructive way, although 
this is not supposed to be my main activity in my current job.
> BTW, the Frama-C manual should be linked in the documentation section on
> http://frama-c.com/support.html.
>   
You mean http://frama-c.com/download/user-manual-Boron-20100401.pdf? 
You're right it is missing, thanks for reporting the problem.

- Claude

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