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



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