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

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. I'd much appreciate a
manual that documents which ACSL keywords are implemented in Jessie +
why and which ones aren't. 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. The same is true for C constants (as in const int
n=10;), see "7.2.1 Unsupported C features". I used to do experiments
with test code to discover what features are implemented in Jessie, but
this just takes too much time.

BTW, the Frama-C manual should be linked in the documentation section on
http://frama-c.com/support.html.

-Boris