p is not an int. Maybe change the return type to void and remove the r from the contract?

Changed to *p.

I think this is trying to show something about ensures with returns?

The paragraph to which this example is attached:

If a postcondition odr-uses a parameter in its predicate and the function body makes direct or indirect modifications of the value of that parameter, the behavior is undefined

suggests it's trying to show that it's ok to refer to a parameter in an ensures when the function body doesn't modify it. The r is extraneous here, as is the int return value.

(Mind you, I'm unsure how the example in [dcl.attr.contract.syn]/6:

void push(int x, queue & q)
  [[expects: !q.full()]]
  [[ensures: !q.empty()]]
{
  /* ... */
  [[assert: q.is_valid()]];
  /* ... */
}

is supposed to ensure !q.empty() without "directly or indirectly modifying the value" of q - but this particular example seems sensible.)

The intent here is that the "value of the parameter" for a reference parameter is just the lvalue to which the reference is bound (which obviously cannot change during the execution of the function). Put another way, evaluating the postcondition in the caller with the values that it passed in should do the same thing as evaluating it in the callee. Can you open a separate editorial issue for that?

Can you open a separate editorial issue for that?

Filed as #2669.

Updated accordingly.