Closed
Description
CBMC version: 5.67.0
Operating system: N/A
We need to describe pointers that may overlap, for example an array and a pointer within that array. Currently, we have prototype same_space
to express this as follows:
bool same_space(const void *a, const void *b) {
size_t a_size = __CPROVER_OBJECT_SIZE(a);
size_t a_offset = __CPROVER_POINTER_OFFSET(a);
void *a_base = a - a_offset;
size_t temp = nondet_size_t();
size_t b_delta = MIN(temp, a_size - ((size_t) 1));
return (b == a_base + b_delta);
}
The issue is that any proof that uses this primitive must disable the pointer-primitive-check
CBMC flag, which is something that should be used in memory safety proofs. We need to disable the flag in order to use the __CPROVER_OBJECT_SIZE
and __CPROVER_POINTER_OFFSET
functions. We should be able to resolve this temporarily by just disabling the flag in a pragma, but this is not supported. There is a GitHub issue addressing this here.