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

[Frama-c-discuss] Predicate call not listed in jessie gui



Hello,

I would like to ask, whether the following is known and what needs to be done to fix my problem.

I have following swap-Function:

/*@
    predicate swapped {L1, L2}(int* a, int* b) =
        \at(*a, L1) == \at(*b, L2) &&
        \at(*b, L1) == \at(*a, L2);
*/
/*@
    requires \valid(a);
    requires \valid(b);
    assigns *a;
    assigns *b;

    ensures *a == \old(*b);
    ensures *b == \old(*a);
    ensures swapped{Here, Old}(a,b);
*/
void swap (int* a, int* b )
{
    int c = *a;
    *a = *b;
    *b = c;
}

When proving with jessie gui, I do not get any error but the predicate-call is neither listed nor does it seem to be proven.

Sincerely

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