Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Non-terminating loops

  • Subject: [Frama-c-discuss] Non-terminating loops
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Thu, 27 May 2010 22:42:10 +0200
  • In-reply-to: <1274979944.3488.36.camel@iti27>
  • References: <1274979944.3488.36.camel@iti27>
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