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] Frama-C / Jessie-Plugin

  • Subject: [Frama-c-discuss] Frama-C / Jessie-Plugin
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Fri, 23 Jan 2009 11:33:43 -0000
 

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