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

[Frama-c-discuss] assigns problem, latest Release



hello,

I would like to know wether I missed something in the following algorithm because I cannot prove the assigns clause.

I had this problem on the beta release before.

/*@
      requires 0 <= length;
      requires disjoint_arrays(a, dest, length);
      requires \valid_range (a, 0, length-1);
      requires \valid_range (dest, 0, length-1);

      assigns dest[0..length-1];
      ensures  \forall integer i; 0 <= i < length ==> dest[i] == \old(a[i]);
    */

    int copy_array (int* a, int length, int* dest)
{

    int index_a = 0;
    int index_dest = 0;

    /*@
    loop invariant 0 <= index_a <= length;
    loop invariant index_dest == index_a;
    loop invariant 0 <= index_dest <= length;

    loop invariant \forall integer k; 0 <= k < index_a ==> \at(a[k],Pre) == dest[k];
    loop assigns dest[0 .. index_a-1];
    */

    while (index_a != length)
    {
        dest[index_dest++] = a[index_a++];
    }

    return index_dest;
}


Cheers Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090107/d8ad4419/attachment.htm