test/mystrncat.c

   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
   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