Avoid null-pointer arithmetic

[feliperodri]

Issue #, if available:
N/A.

Description of changes:
This PR contains two changes:

1. Avoid null-pointer arithmetic.
2. Disable pointer-overflow check for slow proofs.

We have run CBMC 5.30.1 on all proofs in ESDK-C. We must fix these issues before we update CBMC version in CI.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Check any applicable:

• Were any files moved? Moving files changes their URL, which breaks all hyperlinks to the files.

[feliperodri]

Ref.: #704

[robin-aws]

Would you mind adding a bit more context to the PR description (and hence the actual commit) about this being for forwards compatibility with CBMC 5.29?

[robin-aws]

Just to double check my understanding: this just makes these functions opaque to CBMC, which happens to make the proof less expensive?

[feliperodri]

This improves our coverage metric, by discarding functions that are unreachable for this proof. The else branch in field_sized is unreachable, so these functions are never called; however, our coverage analysis still considers this path in the coverage metric. By removing this unreachable functions, we improve coverage metric. If they ever become reachable, our report will through a warning.

[alex-chew]

Of the function bodies removed here, it looks like only aws_byte_cursor_advance appears directly in the else branch in question. Is it sufficient to remove just that function body, or do we need to manually list all the other functions that are transitively called, as done here?

[feliperodri]

@alex-chew we only need to specify the functions that are directly included in the path, you're correct. I updated the list of these function for the aws_cryptosdk_serialize_frame proof and add a comment explaining why we do this.

[feliperodri]

aws_byte_cursor_read_be32 and aws_byte_cursor_read_be64 functions are included in the coverage metric because of field_helper, but we also never reach the else branch there either.