--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] alt-ergo silently ignored / any idea?



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