4 /*@nullterminated@*/ char * strcpy (char * tmp1, /*@nullterminated@*/
6 /*@nullterminated@*/ char * LCLstrcpy (char * tmp1, /*@nullterminated@*/
9 #define strcpy LCLstrcpy
10 /*@nullterminated@*/ char * NotdefinedLCLstrcpy (int * tmp1,
11 /*@nullterminated@*/ char * tmp);
14 // char *my_malloc(int);
16 // /*@null@*/ /*@nullterminated@*/char *fmakeword() {
19 // word = my_malloc(1);
25 /*@nullterminated@*/ char * test1 (char * p1)
27 // p1 = NotdefinedLCLstrcpy (p1, "bob");
28 p1 = LCLstrcpy (p1, "bob");