If f is a field of an object o, we should give a meaning to a writes clause of the form

_(writes &o->f)

It would be convenient, if this writes clause would allow unwrapping o but not changing any other field than f (plus, of course, the corresponding framing on the caller's side). This would allow to safe a lot of \unchanged(...) post-conditions for all those fields that did not change.