Exercise 3.2.5.3: separation of pointer arguments not really required

[wizeman]

In exercise 3.2.5.3 (addition of pointed values) part 2, this is the solution provided:

#include <limits.h>

/*@ 
  requires INT_MIN <= *p + *q <= INT_MAX ;
  requires \valid_read(p) && \valid_read(q) && \valid(r) ;
  requires \separated(p, r);
  requires \separated(q, r);
  assigns *r ;
  ensures *r == *p + *q ;
*/
void add(int *p, int *q, int *r){
  *r = *p + *q ;
}

However, I was able to prove this function to be correct (as well as the examples that call this function) without requiring the separation between pointer arguments, just with a slightly different postcondition:

/*@
    requires \valid_read(a) && \valid_read(b) && \valid(r);
    requires INT_MIN <= *a + *b <= INT_MAX;

    assigns *r;

    ensures *r == \old(*a) + \old(*b);
 */
void add(int *a, int *b, int *r) {
  *r = *a + *b;
}

I'm just showing this in case you prefer this solution, or in case the exercise actually consisted in identifying the separation between pointer arguments (which as you can see, it's not really required).

[AllanBlanchard]

This contract can indeed be validated, but note that it does not prevent the function to modify *a and *b. Thus, I should add a sentence about the fact that *p and *q must remain unchanged.

Thank you.