--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on January 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C / Jessie-Plugin



 

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