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] Problem with Why and Pointers

  • Subject: [Frama-c-discuss] Problem with Why and Pointers
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Mon, 20 Apr 2009 11:13:27 +0200
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