#include <vcc.h>
#include <limits.h>

void memcopy (int *src, int *dst, unsigned len)
  _(requires \thread_local_array(src,len))
  _(writes \array_range(dst, len))
  _(ensures \forall unsigned k; 0 <= k < len ==> dst[k] == \old(src[k])) {
  unsigned i = 0;
  while (i < len)
  _(invariant \forall unsigned k; 0 <= k < i ==> (dst[k] == \old(src[k]) && i <= len)) {
    dst[i] = src[i];
    i++;
  }
  return;
}