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

[Frama-c-discuss] fool the tool



Hello and a happy new year,

today I am trying to modify an implementation and still concur with the function contract.

Therefore following code first:
/*@
    requires 0 <= length;
    requires \valid_range (a, 0, length-1);
    requires \valid_range (b, 0, length-1);

    assigns \nothing;
    
    behavior equal:
        ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]);
    behavior not_equal:
        ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]);
*/
int equal_array (int* a, int length, int* b )
{
    int index_a = 0;
    int index_b = 0;
    /*@
        loop invariant 0 <= index_a <= length;
        loop invariant 0 <= index_b <= length;
        loop invariant index_a == index_b;

        loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k];

    */
    while ( index_a != length )
    {
        if (a[index_a] != b[index_b])
            return 0;
        ++index_a;
        ++index_b;
     }
    return 1;
}

Since I am using "assigns \nothing;" I expect the term \old() in comparison to be obsolete.

But as I recall, assigns \nothing allows temorary modification, as long as the content of the elements mentioned in the parameter list of the function is restored before termination.

So I modified the algorithm, to alter the memory and restore it, allowing the algorithm to return allways "true":

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

    assigns \nothing;
    
    behavior equal:
        ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]);
    behavior not_equal:
        ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]);
*/
int equal_array (int* a, int length, int* b )
{

    int save_array_a[length];
    int save_array_b[length];

    /*@ 
        loop invariant 0 <= i <= length;
        loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k] == 0;
        loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k];
        loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k];
    */
    for(int i = 0; i < length; i++)
    {
        save_array_a[i] = a[i];
        save_array_b[i] = b[i];
        a[i] = 0;
        b[i] = 0; 
    }

    int index_a = 0;
    int index_b = 0;
    /*@
        loop invariant 0 <= index_a <= length;
        loop invariant 0 <= index_b <= length;
        loop invariant index_a == index_b;
        loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k];
    */
    while ( index_a != length )
    {
        if (a[index_a] != b[index_b])
            return 0;
        ++index_a;
        ++index_b;
   }


    /*@
        loop invariant 0 <= i <= length;
        loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k];
        loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k];
    */
    for(int i = 0; i < length; i++)
    {
        a[i] = save_array_a[i];
        b[i] = save_array_b[i]; 
    }
    return 1;
}


My problem:

I cannot invoke the Jessie gui, it stops with the message:

equal_array.c:6: Warning: Variable-sized local variable save_array_a
equal_array.c:7: Warning: Variable-sized local variable save_array_b
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
No code for function __builtin_alloca, default assigns generated
Producing Jessie files in subdir equal_array.jessie
File equal_array.jessie/equal_array.jc written.
File equal_array.jessie/equal_array.cloc written.
Calling Jessie tool in subdir equal_array.jessie
Generating Why function equal_array
File "jc/jc_interp.ml", line 861, characters 11-11:
Uncaught exception: File "jc/jc_interp.ml", line 861, characters 11-17: Assertion failed
Jessie subprocess failed:    jessie  -why-opt -split-user-conj  -v       -locs e
qual_array.cloc equal_array.jc


My question:

Is this indended, signaling me to stop fooling around or am I missing something to invoke the gui properly.


Cheers

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