CBMC misbehaves in functions with pointer arithmetic computation

[AmPaschal]

We found some arbitrary behavior when using CBMC to verify a function with pointer arithmetic.

For example, in the code below.

void harness() {

    uint8_t bufsize;

    __CPROVER_assume(bufsize > 0);

    uint8_t *data = malloc(bufsize);

    __CPROVER_assume(data != NULL);

    uint8_t datasize;

    __CPROVER_assume(datasize > 0);

    if (datasize > bufsize) {
        return;
    }

    uint8_t *data2 = data + datasize;

    data2++; // Interestingly, if you remove this line, the memcpy read violation disappears

    uint8_t expected_len = 4;
    uint8_t dest[expected_len];

    uint8_t diff = (data2 - data); // In the trace, the value is diff is arbitrary

    if (diff + expected_len > bufsize) {
        // This validation is supposed to prevent the OOB read in the memcpy below.
        return;
    }

    memcpy(dest, data2, expected_len);

}

The validation if (diff + expected_len > bufsize) { is supposed to ensure that data2 contains up to expected_len bytes of data.
However, CBMC still reports an OOB read error in the memcpy line.
Looking at the error trace, we find that the diff computed is always arbitrary, regardless of the values of data and data2.

We tested this using CBMC v6.3.1

[kroening]

The data2++ moves the pointer out of the bounds of the object (you are allowed to point to the element that is just beyond the bound). This is hence already undefined behaviour.