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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Thu, 27 May 2010 21:16:33 +0200
  • In-reply-to: <1274979944.3488.36.camel@iti27>
  • References: <1274979944.3488.36.camel@iti27>
Hello,

On Thu, May 27, 2010 at 7:05 PM, Boris Hollas
<hollas at informatik.htw-dresden.de> 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.

I tried it and it worked for me.

Pascal

PS: what's wrong in this answer? It doesn't say exactly what program
I tried, it doesn't provide the command-line I used, and it doesn't tell
what results I obtained and interpreted as meaning that I had obtain
the result I wanted. Someone trying to reproduce what I did
has to write his/her own program and won't even know if he/she is
seeing the same thing I was (and I am in fact misinterpreting
the results).

It is your choice whether to report this as a bug or here (as a reminder,
bug reports are seen by fewer people but remain "open" until a
competent person has looked at them, which is not true for mailing
list postings). If you ask about a bug or something that may be one
in the mailing list, you still have to provide all the information that makes
a good bug report.

FWIW, I used the program:

int rand(void);

int x;

#pragma JessieTerminationPolicy(user)
void main(void)
{
  while(rand()<100)
    x = x;
}

and the command-line "frama-c -jessie u.c".
I obtained an empty list of VC, each of which was proved.

The ACSL "terminates" clause does not appear to be
supported in Jessie, from the result obtained when trying
the same program in which the pragma is replaced with

/*@
  terminates \false ;
*/

In this case, the command-line "frama-c -jessie t.c"
generates a proof obligation

0<0

There should be a "false" (from the "terminates" clause)
in the hypotheses to prove this property, but there doesn't
seem to be.

NB: this is all using Frama-C 20100401 with a patched version
of Why 2.23.

Pascal