Pointer encoding limits address space to 24bits for ILP32

[peterschrammel]

The following fails when checking with --ilp32 (for nbytes >=2^24)

uint32_t nondet_uint32_t();

void mk_char_array() {
uint32_t nbytes = nondet_uint32_t();
char memory[nbytes];
char *start = &memory[0];
char *end = &memory[nbytes];
uint32_t diff = end - start;
__CPROVER_assert(diff == nbytes, "Check size match");
}

It's rare to allocate arrays of that size in software, and few people use ILP32, however, the restriction is an unnecessary artefact of the encoding that CBMC uses (upper 8 bits for object reference, remaining bits for offset within the object)...
The problem doesn't occur with LP64 (64-8 > 48).

Issue raised by Nathan Chong, ARM.