--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on January 2009 ---
Hi everybody! I think I found a problem in the generation of proof-obligations using Jessie Plug-in. But I don?t know if it is a bug, or if the problem is mine ( probably because I don?t understand the memory model that is behind Frama-C to Why translation). I made a simple example of the problem I want to expose: /*@ requires len>=0 && @ \valid_range(a,0,len-1) && @ \valid_range(b,0,len-1); @ ensures (a == \at(a,Old) + len) && (b == \at(b,Old) + len); @*/ void func(const unsigned long len,const unsigned char *a, unsigned char *b) { int i; i=(int)(len); if (i) { /*@ loop invariant 0<=i<=len && @ a == \at(a,Pre) + (len-i) && @ b == \at(b,Pre) + (len-i); @ loop variant i; @*/ while (1) { a[0] == b[0] + 1; a++; b++; if (--i == 0) break; } } } I found a problem on running these example in Frama-C and in generating the proof-obligations. If a post-condition is added, are generated more post-conditions that would be probable to generate. That is, are generated intermediate post-conditions that I don?t understand why they are generated. When post-condition is not added, the proof-obligations seems to well generated. Another thing that I had noted is that if I add an assertion at the end of the loop, the proof-obligation related to this assertion is duplicated. If anybody can help me, I would appreciate. Best regards, B?rbara -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090121/1689ebff/attachment-0001.htm