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

[Frama-c-discuss] multiple functions, why error



Hello, now I have a rather complex example, which I need some advice with before posting it on the BTS

The function reverse uses a swap function to reverse the elements of an array:

#include "swap.h"
/*@
    requires 0 <= length;
    requires \valid_range (a, 0, length-1);
    ensures \forall integer k; 0 <= k < length ==>
    \old(a[k]) == a[length-1-k] &&
    a[k] == \old(a[length-1-k]);
*/
void reverse_array (int* a, int length)
{
    int index_a = 0;
    int index_backwards = length;

/*@
    loop invariant 0 <= index_a <= length;
    loop invariant 0 <= index_backwards <= length;
    loop invariant index_a == length - index_backwards;

    loop invariant \forall integer k; 0 <= k < index_a ==> \at(a[k],Pre) == a[length-1-k] &&
    a[k] == \at(a[length-1-k],Pre);
*/
    while ((index_a != index_backwards) && (index_a != --index_backwards))
        swap_user (&a[index_a++], &a[index_backwards]);
}

File "swap.h"
========
/*@
    requires \valid(a);
    requires \valid(b);
    ensures *a == \old(*b);
    ensures *b == \old(*a);
*/
void swap_user (int* a, int* b );

File "swap.c"
========
#include "swap.h"
void swap_user (int* a, int* b )
{
    int c = *a;
    *a = *b;
    *b = c;
}

When invoking the Gui for reverse_array()
I get the error:
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
No code for function swap_user, default assigns generated
Producing Jessie files in subdir reverse_array.jessie
File reverse_array.jessie/reverse_array.jc written.
File reverse_array.jessie/reverse_array.cloc written.
Calling Jessie tool in subdir reverse_array.jessie
Generating Why function reverse_array
Calling VCs generator.
make[1]: Entering directory `/cygdrive/d/Eigene Dateien/StudienUnterlagen/Praxis
semester/SVN/trunk/Framac/own-examples/ProvableSTL/reverse/reverse_array.jessie'

gwhy-bin [...] why/reverse_array.why
Computation of VCs...
File "why/reverse_array.why", line 1158, characters 101-117:
Application to int_P_int_M_a_22 creates an alias
make[1]: *** [reverse_array.stat] Error 1
make[1]: Leaving directory `/cygdrive/d/Eigene Dateien/StudienUnterlagen/Praxiss
emester/SVN/trunk/Framac/own-examples/ProvableSTL/reverse/reverse_array.jessie'
Jessie subprocess failed: make -f reverse_array.makefile gui



I would like to know whether the mistake is mine or if I have to post on the BTS


Cheers Christoph

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