#include <string.h>

#define MAXNAME 30

/* Copy string and add "<--" */
void copy(/*@unique@*/char *from, /*@out@*/char *to, size_t size)
     /*@requires ??? @*/
{
  strncpy(to,from,size);
  to[size-1] = '<';
  to[size+0] = '-';
  to[size+1] = '-';
  to[size+2] = '\0';
}

main()
{
  char name[MAXNAME+7], name2[MAXNAME] = "antidisestablishmentarianism!";

  copy(name2,name,MAXNAME);
  printf("Input : %s\nOutput: %s\n",name2,name);

  return 0;
}