Update Proof Guide to cover use of OBJECT_UPTO rather than OBJECT_WHOLE

[rod-chapman]

The Proof Guide document (cbmc/proofs/proof_guide.md) talks of using the OBJECT_WHOLE macro within ASSIGNS contracts. We now know this is unwise, and that the OBJECT_UPTO macro is almost always a better choice.

The guide should be updated to explain why this is so, and update the existing examples to use OBJECT_UPTO where appropriate.

I also suggest adding a sub-section under "proof patterns" called "Updating composite objects" that gives guidance on how to write contracts for functions that update a composite object (e.g. an array or a struct) via a mutable by-reference parameter.

[rod-chapman]

Also remember to mention the use of

--slice-formula
--no-array-field-sensitivity
--arrays-uf-always

switches and where/when to try these.

[hanno-becker]

@rod-chapman I'm assining you to this, ok?