#include #include #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()