#include <stdio.h>
#include <string.h>
#define BUFSIZE 10

int main(/*@unused@*/ int argc,
         /*@unused@*/ char * argv []
        )
  /*@-modfilesys@*/
  {
    /*@unused@*/
    char pwd[18] = "It is top secret!";
    /*@-initallelements@*/
    char target [BUFSIZE] = { '\0' };
    /*@+initallelements@*/
    char source [17] = "0123456789ABCDEF";

    printf("source: %s\ntarget: %s\n",source,target);
    strncpy(target, source, (size_t) BUFSIZE );
    printf("source: %s\ntarget: %s\n",source,target);
    return 0;
  }