CBMC: Understand and use the correct shape of stub-harnesses for spec-proofs

[hanno-becker]

When we verify specs, we still need to provide stub harnesses invoking the function-under-proof. Morally, it seems that those harnesses should be irrelevant, but #306 (specifically this commit a95a2ce) suggest that this may be wrong: In this commit, the spec for poly_add() does not provide any bound on the r buffer, and yet the proof goes through. This is likely because the harness allocates the data on the stack, which may inadvertently add to the pre-conditions of poly_add -- it's likely that an uninitialized poly* should have been passed.

• Understand what the correct shape of harnesses for spec-proofs is
• Apply needed changes throughout
• Adjust the CBMC proof guide accordingly

[hanno-becker]

@rod-chapman Can you chime in? Is the suspicion correct that the harness should not pass pointers to stack allocated variables?

[rod-chapman]

I agree that the harness should infer a little information as possible, so passing an unitialized pointer rather than a pointer to a stack-allocated local object feels OK to me, assuming the proofs all succeed. We need to confirm this advice with CBMC team, then update the Proof Guide accordingly.

[hanno-becker]

The CBMC team has confirmed this.

[hanno-becker]

@rod-chapman Let me know when you have updated the proof guide, and then we can close this.