memcpy() does not take pointer offset into account

[david-k]

Hi,
memcpy() does not seem to take pointer offsets into account, e.g. memcpy(dest + 1, src + 1, sizeof(int)) compiles to the equivalent of memcpy(dest, src, sizeof(int)).

void test()
{
    int a = 1;
    int b = 2;
    int dest[2];

    memcpy(dest, &a, sizeof(int));
    memcpy(dest + 1, &b, sizeof(int));

    assert(dest[1] == b); // Erroneously fails in CBMC 5.8, but works as expected in CBMC 5.6
}

In CBMC 5.6, memcpy() was implemented using a loop, but I think in 5.7 or 5.8 this was changed to using __CPROVER_array_copy/__CPROVER_array_replace. Could this have anything to do with the error?

[tautschnig]

Yes, the changes to __CPROVER_array_{copy,replace} introduced that bug. It's fixed by #1800, once merged.

[david-k]

Great, thank you!

[david-k]

I just tried out the referenced commit but it seems to only work with char: the test in the commit breaks if int is used, and my example above works if I use char.

[tautschnig]

Thank you very much for insisting! There is another bug lingering around, I'm trying to figure out what's going on there.

[tautschnig]

I believe this is now actually fixed by #1800.

[david-k]

Yes, works in my use cases!