--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on April 2009 ---
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