qsort4.c uses memcpy illegally

[andrew-appel]

qsort4.c has a bug: it can call memcpy with overlapping source and destination arguments. This is "undefined behavior" in the C standard. Therefore the cbench-vst verification of qsort4 has one admitted lemma, for the case where we must assume that memcpy(dest,src,size) has no effect when dest=src.

Here's the code:

   if (i <= j) {
        memcpy(tmp, a(i), size);
        memcpy(a(i), a(j), size);
        memcpy(a(j), tmp, size);
        i++; j--;
      }

and indeed it is possible that i==j -- just sort a 2-element list [0;1].