--- layout: fc_discuss_archives title: Message 111 from Frama-C-discuss on May 2010 ---
Hello Claude, > 1) in Beryllium-2 and Why 2.21, the pragma JessieTerminationPolicy is > not available yet It seems it is, because Pascal's example works for me. > 3) terminates clause is not supported by Jessie even in the most recent > version. This is documented and if you look carefully you should see a > warning. In both the acsl-beryllium2 and the acsl-boron documentation terminates is marked as "Experimental" in section "2.5.4 Non-terminating functions". If it is not supported yet, it should be indicated. I understand "Experimental" as something that has been implemented, but may not work in all circumstances. 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. -Boris