CBMC version: 5.12 (cbmc-5.12-51-g051911e31)
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc memcopycrash.c
What behaviour did you expect: program finished successfully
What happened instead: Invariant check failed
Source file memcopycrash.c:
#include <assert.h>
void *memcpy();
struct offsetE
{
char H;
char V;
};
struct comp_t
{
struct offsetE offsets[2];
unsigned m_size[2];
};
int main(void)
{
struct comp_t comp;
struct offsetE T8[2] =
{
{((char)1),((char)1)},{((char)0),((char)1)}
};
(void)memcpy((char *)&(comp.offsets), (char *)&T8, 4);
assert(comp.m_size[0] == 8);
return 0;
}
Backtrace is attached.
backtrace.log