1 void mystrncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n) 2 /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/ 3 /*@ensures MaxRead(result) >= (MaxRead(s1) + n); @*/; 4 func(char * str)5 void func(char *str) 6 { 7 char buffer[256]; 8 char *b; 9 10 b = malloc(256); 11 assert(b != NULL); 12 mystrncat(buffer, str, sizeof(buffer) - 1); 13 mystrncat(b, str, sizeof(buffer) - 1); 14 15 free (b); 16 return; 17 } 18 19