--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on May 2010 ---
Hi Boris, Although Pascal's answer is a bit, let me say, "pascal-cuoqesque", it contains all the answers: 1) in Beryllium-2 and Why 2.21, the pragma JessieTerminationPolicy is not available yet 2) I don't know any workaround, except ignoring the unsolved VC Thus I would recommend to upgrade to Boron/Why-2.26, and use #pragma JessieTerminationPolicy(user) and finally: 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. Let me finally remind that Jessie/Why is open source software, so anybody willing to contribute the support of terminates clauses is welcome. - Claude On 05/27/2010 07:05 PM, Boris Hollas wrote: > I have a loop that I don't want Jessie to generate a VC for termination. > With "terminates \false", Jessie still tries to prove termination. Is > there anything that can be done about this? I use the Beryllium 2 > distribution. > > The loop is of the form > while(rand()< 100) {...} > which eventually terminates, but it requires probability theory to prove > this. > > -Boris > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss