#include <strings.h>
#include <stdio.h>

#define BUFSIZE 10
int main(int argc, char * argv [])
  /*@requires maxRead(argv) >= 1 @*/
  /*@-modfilesys@*/
  {
    /*@-initallelements@*/
    char buffer [BUFSIZE] = {'\0'};
    /*@+initallelements@*/
    if ( ( argc > 0 )  && (argv != NULL) )
      {
        strncpy(buffer, argv[1], (size_t) (BUFSIZE-1));
        printf("%s\n",buffer);
      }
    return 0;
  } // end main()