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

[Frama-c-discuss] Pointers in Frama-C/Why



 

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