frama-calt-ergo

frama-c wp plugin fails to validate the swap function from the manual

How to make frama-c -wp verify the example from the wp manual - a trivial swap function (swap.c):

/* @ requires \valid(a) && \valid(b);
   @ ensures A: *a == \old(*b);
   @ ensures B: *b == \old(*a);
   @ assigns *a,*b;
   @*/
void swap(int * a, int * b);

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

The invocation

$ frama-c -wp -wp-rte swap.c

gives:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function swap
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_4 : Unknown (174ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_2 : Unknown (160ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Unknown (154ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Unknown (220ms)
[wp] Proved goals:    0 / 4
     Alt-Ergo:        0  (unknown: 4)

I wonder why

  1. the number of goals is different (4 vs. 9) in my try versus the manual?
  2. Alt-Ergo (and in fact, none of cvc3, gappa, simplify, verit, yices, z3) was not able to discard any of these 4 proof obligations?

I use the latest OPAM installation:

An example of proof obligations, passed to alt-ergo by wp: 

goal swap_assert_rte_mem_access:
  forall t : int farray.
  forall a_1,a : addr.
  linked(t) ->
  (region(a.base) <= 0) ->
  (region(a_1.base) <= 0) ->
  valid_rd(t, a, 1)
Solution

  • You made a mistake when you copied the specification of swap from the WP manual. (The next version will use a font that permits copy-pasting.) There must be no space between the beginning of the C comment and the @ in the ACSL specifications; otherwise the comment is interpreted as a simple comment. Thus, you are effectively trying to prove

    void swap(int * a, int * b);

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

    which is course impossible because a and b may not be valid pointers.

    The correct specification is 

    /*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == \old(*b);
  @ ensures B: *b == \old(*a);
  @ assigns *a,*b;
  @*/
void swap(int * a, int * b);

    When using Frama-C on small examples, you should probably be using the GUI interface (frama-c-gui). This way, you will see your source code after normalization, what RTE have been added, etc.