Dangling pointers in Rust are considered valid by Miri as long as they are not null, aligned, not deallocated, not out of bounds (if they have the provenance of some allocation) and we don't read or write more than zero bytes from/to the memory location they point to. By contrast, CBMC considers reading and writing from/to such dangling pointers to be UB, for example in memcmp(..., ..., 0).

This was originally discovered in #1489 but the same problem could occur with other functions than memcmp, so we should probably figure out a better way to deal with it. Previous discussion:

• discovery and some discussion: Investigate failed check in memcmp #1489
• mitigation for memcmp: Mitigate issue with dangling pointers and memcmp #1526
• two examples that we should reject, but now accept due to shortcomings of the mitigation PR: Investigate failed check in memcmp #1489 (comment), Mitigate issue with dangling pointers and memcmp #1526 (comment)
• CBMC issue discussing pointer semantics: --pointer-primitive-check fails on __CPROVER_r_ok(ptr, 0) when ptr = malloc(0) diffblue/cbmc#7064.
• In particular, Daniel Kröning says: "Note that memcpy doesn't accept invalid pointers even when the size is zero." (--pointer-primitive-check fails on __CPROVER_r_ok(ptr, 0) when ptr = malloc(0) diffblue/cbmc#7064 (comment)). So the interpretation of the C standard seems to differ here.
• Documentation of pointers in CBMC: http://cprover.diffblue.com/memory-primitives.html