--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2012 ---
Hi Virgile, first, thanks for the fast response! My bad, I should have given the following information: Here is the code to check (from the WP manual): /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b) ; @ ensures B: *b == \old(*a) ; @ assigns *a,*b ; @*/ void swap(int *a,int *b) { int tmp = *a ; *a = *b ; *b = tmp ; return ; } Here the result that is to be expected (from the WP manual): # frama - c - wp -wp - rte swap . c swap2 . c [ kernel ] preprocessing with " gcc -C -E -I . swap . c " [ kernel ] preprocessing with " gcc -C -E -I . swap2 . c " [ rte ] annotating function swap [ wp ] [ WP : simplified ] Goal s t o r e _ s w a p _ f u n c t i o n _ a s s i g n s : Valid [ wp ] [ Alt - Ergo ] Goal s t o r e _ s w a p _ a s s e r t _ 4 _ r t e : Valid [ wp ] [ Alt - Ergo ] Goal s t o r e _ s w a p _ a s s e r t _ 3 _ r t e : Valid [ wp ] [ Alt - Ergo ] Goal s t o r e _ s w a p _ a s s e r t _ 2 _ r t e : Valid [ wp ] [ Alt - Ergo ] Goal s t o r e _ s w a p _ a s s e r t _ 1 _ r t e : Valid [ wp ] [ Alt - Ergo ] Goal s t o r e _ s w a p _ p o s t _ 2 _ B : Valid [ wp ] [ Alt - Ergo ] Goal s t o r e _ s w a p _ p o s t _ 1 _ A : Valid Here is the result I get: $ frama-c -wp -wp-rte -wp-proof alt-ergo /c/src/wp.c [kernel] preprocessing with "gcc -C -E -I. c:/src/wp.c" [rte] annotating function swap [wp] [WP:simplified] Goal store_swap_function_assigns : Valid Expected and actual are not the same so I stay to my point. :-) Thanks in advance for any hint, this is driving me crazy! Sylvain