Finer-grained writes clauses


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.


stobies wrote Mar 22, 2012 at 8:22 PM

Use skinny expose for the moment.