Why WP can't deduce "else" close?

Question

I'm trying to write the specification for a function which takes 2 pointers to int and put the smaller value to the first pointer and the other to the second.

Here is the code and the specification:

/*@
   requires \valid(a) && \valid(b);

   assigns *a, *b;

   ensures *a >  *b ==> *a == \old(*b) && *b == \old(*a);
   ensures *a <= *b ==> *a == \old(*a) && *b == \old(*b);
*/
void order(int * a, int *b) {
  if (*a > *b) {
    int tmp = *a;
    *a = *b;
    *b = *a;
  }
}

And here is the output of frama-c -wp so.c:

[kernel] Parsing so.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_order_post_2 : Unknown (Qed:4ms) (366ms)
[wp] Proved goals:    3 / 4
  Qed:             2  (0.40ms-2ms-5ms)
  Alt-Ergo:        1  (30ms) (16) (unknown: 1)

WP can't prove the second post-condition, can you explain me why?

Answer 1

It turns out the solution to my question is in Alain Blanchard's tutorial, $3.3.1.1. (here)

In the post-conditions, I'm missing the \old primitives around *a and *b. So the conditions should read:

ensures \old(*a) < \old(*b) ==> *a == \old(*b) && *b == \old(*a) ;
ensures \old(*a) >= \old(*b) ==> *a == \old(*a) && *b == \old(*b) ;

Without the \old, the left parts of the implications are about the values after the function execution.