[splint.git] / test / mystrncat.c

void  mystrncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
     /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/
     /*@ensures MaxRead(result) >= (MaxRead(s1) + n); @*/;

     void func(char *str)
{
  char buffer[256];
  char *b;

  b = malloc(256);
  assert(b != NULL);
  mystrncat(buffer, str, sizeof(buffer) - 1);
  mystrncat(b, str, sizeof(buffer) - 1);

  free (b);
  return;
}
Commit	Line	Data
e5081f8c	1	void mystrncat (/@unique@/ /@returned@/ char s1, char s2, size_t n)
98ed3b22	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