[dcl.attr.contract.cond]/7 states:

If a postcondition odr-uses ([basic.def.odr]) a parameter in its predicate and the function body makes direct or indirect modifications of the value of that parameter, the behavior is undefined [ Example: ...

Yet the example in [dcl.attr.contract.syn]/6 includes a function push:

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

which seemingly must "directly or indirectly modify the value" of its parameter q to ensure the postcondition !q.empty() holds. If - as suggested to me by @zygoloid - the intent is that the value of a parameter of reference type is simply the glvalue to which the reference is bound, and not the result of lvalue-to-rvalue conversion on that glvalue (which we would normally refer to as "the value of q") then the wording in [dcl.attr.contract.cond]/7 needs clarification.