--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on April 2009 ---
Hello again, I have solved my most recent question but I am not sure whether it is due to an inconsistency in the gui. The function: /*@ requires 0 <= length; requires \valid_range(a, 0, length-1); requires \valid_range(b, 0, length-1); 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; int tmp; /*@ loop invariant 0 <= i <= length; loop invariant \forall integer k; 0 <= k < i ==> swapped {Here, Pre}(a+k, b+k); loop invariant \forall integer k; i <= k < length ==> \at(a[k], Here) == \at(a[k], Pre)&& \at(b[k], Here) == \at(b[k], Pre); */ for (;i != length; i++) { /* swap(a+i, b+i); */ tmp = a[i]; a[i] = b[i]; b[i] = tmp; } return i; } I would like to know, if loop invariant \forall integer k; i <= k < length ==> \at(a[k], Here) == \at(a[k], Pre)&& \at(b[k], Here) == \at(b[k], Pre); should be initialized. If everything is fine in spite this fact, I would be very happy. Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090420/32568b06/attachment.htm