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] fool the tool

  • Subject: [Frama-c-discuss] fool the tool
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Wed, 7 Jan 2009 09:57:17 +0100
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