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