--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on April 2009 ---
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