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: Claude.Marche at inria.fr (Claude Marche)
  • Date: Fri, 28 May 2010 17:25:11 +0200
  • In-reply-to: <1275053214.2159.57.camel@iti27>
  • References: <1274979944.3488.36.camel@iti27> <4BFED922.9080101@inria.fr> <1275049412.2159.26.camel@iti27> <4BFFBA4D.80104@inria.fr> <1275053214.2159.57.camel@iti27>
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                    |