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
- Follow-Ups:
- [Frama-c-discuss] Non-terminating loops
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Non-terminating loops
- References:
- [Frama-c-discuss] Non-terminating loops
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Non-terminating loops
- Prev by Date: [Frama-c-discuss] frama graph plugins
- Next by Date: [Frama-c-discuss] Non-terminating loops
- Previous by thread: [Frama-c-discuss] Non-terminating loops
- Next by thread: [Frama-c-discuss] Non-terminating loops
- Index(es):