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

[Frama-c-discuss] Problem with Why and Pointers



Hello, I failed to create a minimal example, so this need to do:

/*@
 predicate swapped {L1, L2}(int* p, int* q) =
  \at(*p, L1) == \at(*q, L2) &&
  \at(*q, L1) == \at(*p, L2);
  
*/

/*@
 requires \valid(p);
 requires \valid(q);
 assigns *p;
 assigns *q;
 
 ensures *p == \old(*q);
 ensures *q == \old(*p);
 ensures swapped {Here, Old}(p, q);
*/
void swap (int* p, int* q )
{
    int c = *p;
    *p = *q;
    *q = c;
}


/*@
 requires 0 <= length;
 requires \valid_range(a, 0, length-1);
 requires \valid_range(b, 0, length-1);
 
 requires a + length < b || b + length < a; 
 
 ensures \forall integer i; 
  0 <= i < length ==> swapped {Here, Old}(a+i, b+i);

*/
int swap_ranges_array(int* a, int length, int* b)
{
 int i = 0;
 /*@
  loop invariant 0 <= i <= length;
  loop invariant a+i != b+i;
  loop invariant \forall integer k;
   0 <= k < i ==> swapped {Here, Pre}(a+i, b+i);
 */
  for ( ; i != length; ++i)
  {
    swap(a+i, b+i);
  }
  return i;
}

When calling this example with jessie gui, I get the message:

File "why/swap_ranges_array.why", line 1152, characters 106-122:
Application to int_P_int_M_a_24 creates an alias
make[1]: *** [swap_ranges_array.stat] Error 1.

I will forward this message to the BTS but would also like to know, what is  necessary
to proof the 
  loop invariant \forall integer k;
   0 <= k < i ==> swapped {Here, Pre}(a+i, b+i);

since
    loop invariant a+i != b+i;
fails to initialize, i have no clue.

Sincerely
Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090420/43dab3d3/attachment.htm