--pointer-primitive-check alarms for valid pointer

[danielsn]

CBMC version: 5.12 (cbmc-5.12-185-g03ab5c75a)
Operating system: OSX
Exact command line resulting in the issue: In the folder tests/cbmc/proofs/s2n_stuffer_copy in the https://github.com/danielsn/s2n/tree/diffblue-cbmc-5335 , run the command make report.
What behaviour did you expect: No errors
What happened instead: pointer in pointer primitive is neither null nor valid in POINTER_OBJECT(__CPROVER_dead_object)

[danielsn]

In particular
https://github.com/danielsn/s2n/blob/diffblue-cbmc-5335/tests/cbmc/proofs/s2n_stuffer_copy/s2n_stuffer_copy_harness.c#L34-L37
We can dereference *from without a problem, but can't check that its readable.

[feliperodri]

I have the same issue on this proof aws_cryptosdk_encrypt_body.
If you run it locally, there is no problem with the dereference, but the __CPROVER_w_ok and __CPROVER_w_ok checks fail.

[danielsn]

@danpoe

[danpoe]

Fix is here: #5336