--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on January 2009 ---
Hi everyone! Can anybody help, and tell me why this code generate four proof-obligations to the post-condition and 5 proof- obligations to the assertion, when it is just supposed to generate only 2 proof-obligations for post-conditions and 3 proof-obligations to the assertion. (Using the predefined option ?why-opt ?split-user-conj is Jessie). /*@ requires len>=0 && @ \valid_range(a,0,len-1) && @ \valid_range(b,0,len-1); @ ensures (\at(a,Here) == \at(a,Old) + len) && @ (\at(b,Here) == \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 (i>0) { a[0] == b[0] + 1; a++; b++; --i; //if (--i == 0) break; } } /*@ assert i==0 && @ a == \at(a,Pre) + (len-i) && @ b == \at(b,Pre) + (len-i); @*/ } I made a post some days ago, but I didn?t get an answer. I supposed that the problem of generating so many proof-obligations was because I was using a ?break?. Here, I?m not using a break, to avoid the intermediate proof-obligations that are generated and are related with the post-condition. In this code I don?t understand the proof-obligations that are generated related with the post-conditions too, because they seem to appear duplicated. Probably there is some inconsistence in the code, because the last proof-obligation is mysteriously proved using Simplify, and I don?t understand how it is provable. If anybody can help, I appreciate a lot. Thanks in advance. Best regards, B?rbara -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090123/bd0527dc/attachment.htm