Improve instrument_call_statement in code contracts to handle all uses of __CPROVER_allocate

[feliperodri]

CBMC version: >5.15
Operating system: Ubuntu 18.04 or macOS Mojave 10.14.6
Exact command line resulting in the issue: N/A.
What behaviour did you expect: N/A.
What happened instead:

I'd like to see handling of all uses of __CPROVER_allocate here. malloc is just one such case invoking __CPROVER_allocate. I'd propose a simple analysis that

1. Checks whether the body of the called function is available,
2. and if it is, whether the body of that function includes a __CPROVER_allocate call.

Suggested in #5403.

[martin-cs]

I believe __CPROVER_allocate to be an internal interface. I think it should only be used in library functions and in modelling the most primitive access to the heap. User code should not call it.

[feliperodri]

@tautschnig you suggested this here. Do you agree with @martin-cs? Should I keep this open?

[feliperodri]

I'll close this for now based on @martin-cs' comment.