--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on May 2010 ---
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