--- layout: fc_discuss_archives title: Message 117 from Frama-C-discuss on May 2010 ---
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 |