1 void mystrncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, int n)
2 /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/
3 /*@ensures MaxRead(result) >= (MaxRead(s1) + n); @*/;
12 mystrncat(buffer, str, sizeof(buffer) - 1);
13 mystrncat(b, str, sizeof(buffer) - 1);