`__CPROVER_allocated_memory` is undocumented

[thomasspriggs]

I have not been able to find any existing documentation of the __CPROVER_allocated_memory intrinsic function. Without documentation of this intrinsic and its current implementation / intended use case it is non-trivial to work out what aspects of its observed functionality are intended or are bugs with the current implementation.

CBMC version:
Operating system:
Exact command line resulting in the issue:
What behaviour did you expect:
What happened instead:

[feliperodri]

@diffblue/diffblue-opensource

[thomasspriggs]

I believe the current plan is to remove it. Therefore adding documentation beyond "This is deprecated. Don't use it." Wouldn't really be useful.

[thomasspriggs]

Aha! Documentation of the current behaviour is here - #7157
See also -

• Document MMIO behaviour #6997
• Add deprecation warning for intrinsic __CPROVER_allocated_memory  #6876
• CBMC does not sufficiently validate __CPROVER_allocated_memory #6871
• Pointer validity checks on __CPROVER_allocated_memory #6695

[tautschnig]

Closing via #7157.