Incorrect assertion failure after memcpy with variable size #5885
Description
CBMC version: cbmc-5.25.0
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc
What behaviour did you expect: Verificaton success
What happened instead: Verification failed
An example is below:
#include <string.h>
#include <assert.h>
int main(void)
{
int src[8], dst[8], delta;
if(delta == 3 || delta == 4)
{
memcpy(dst, src, sizeof(int) * delta);
assert(dst[1] == src[1]);
}
return 0;
}Simplifying the if condition to delta == 3 or delta == 4 works correctly, as does setting delta to a constant value.
The program equation as shown by --program-only looks correct. The relevant equation is:
(43) dst!0@1#1 == byte_update_little_endian({ dst!0@1#1[[0]], dst!0@1#1[[1]], dst!0@1#1[[2]], dst!0@1#1[[3]], dst!0@1#1[[4]], dst!0@1#1[[5]], dst!0@1#1[[6]], dst!0@1#1[[7]] }, 0l, src_n!0@1#2, char [sizeof(signed int) /*4ul*/ * (__CPROVER_size_t)(signed long int)(__CPROVER_size_t)delta!0@1#1])
The verification condition as shown by --show-vcc also looks correct. The relevant formula is:
{-26} main::1::dst!0@1#1 = byte_update_little_endian({ main::1::dst!0@1#1[[0]], main::1::dst!0@1#1[[1]], main::1::dst!0@1#1[[2]], main::1::dst!0@1#1[[3]], main::1::dst!0@1#1[[4]], main::1::dst!0@1#1[[5]], main::1::dst!0@1#1[[6]], main::1::dst!0@1#1[[7]] }, 0, memcpy::1::1::src_n!0@1#2, signedbv[32][8])
My guess is that the translation of byte_update with variable offset to propositional logic is incorrect.