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