/* Copy SRC to DEST.  */
    char *
    strcpy (dest, src)
         char *dest;
         const char *src;
    {
      char c;
      char *__unbounded s = (char *__unbounded) CHECK_BOUNDS_LOW (src);
      const ptrdiff_t off = CHECK_BOUNDS_LOW (dest) - s - 1;
      size_t n;

      do
        {
          c = *s++;
          s[off] = c;
        }
      while (c != '\0');

      n = s - src;
      (void) CHECK_BOUNDS_HIGH (src + n);
      (void) CHECK_BOUNDS_HIGH (dest + n);

      return dest;
    }