typedef unsigned int size_t;

void *
c_memcpy(void *dst, void *src, size_t length)
{
  int i;
  unsigned char *dp = dst;
  unsigned char *sp = src;

  for (i=0; i<length; i++)
    *dp++ = *sp++;
  return dst;
}

void Frama_C_memcpy(void *dst, void *src, size_t length);

char s[10000], d[10000];

main()
{
  // Make problem representative
  for (int i=0; i<100; i++)
    s[100*i] = i;

  // Time one or the other
  //  c_memcpy(d, s, 10000);
  Frama_C_memcpy(d, s, 10000);

  // Check that d contains the right thing
  Frama_C_dump_each();
  return 0;
}