Model checking allocation failure

[tedinski]

We should introduce a flag (and an associated proof harness annotation) to enable --malloc-can-fail in CBMC.

At first, this might seem useless, because many std data structures will simply panic on allocation failure. (And without #692, this just means all such proof harnesses would just have failures that are unavoidable.)

But there is no-std Rust code out there that might be very interested and could use this feature.

• [ ] Make sure we have an example customer to sanity check the feature before we add anything.
• [ ] Add a command line flag that's simply passed down to CBMC.
• [ ] Add a proof harness attribute to enable this feature on a per-harness basis.

[tedinski]

Also note that because we currently override std to override macros definitions, we'll have to do some additional work to specifically support verifying no_std code. That prerequisite might make this not totally "Exp: easy" anymore.