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



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