#include <string.h>

#define MAXNAME 30

main(int argc, char *argv[])
     /*@requires maxRead(???) >= ???@*/
{
  char progname[MAXNAME];


  strncpy(progname,argv[0],MAXNAME);

  return 0;
}