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] multiple functions, why error

  • Subject: [Frama-c-discuss] multiple functions, why error
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Wed, 7 Jan 2009 16:10:40 +0100
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