[splint.git] / test / simplebufferConstraintTests / m.c

extern /*@null@*/ /*@out@*/ /*@only@*/ void *mymalloc (size_t size) /*@*/
     /*@ensures MaxSet(result) == (size - 1) @*/ ;
  
void t()
{
char *f;

f = mymalloc (3);
f[2] = '2';
free (f);
}
Commit	Line	Data
41320549	1	extern /@null@/ /@out@/ /@only@/ void mymalloc (size_t size) /@*/
dcaf75ea	2	/@ensures MaxSet(result) == (size - 1) @/ ;
41320549	3
	4	void t()
	5	{
	6	char *f;
	7
	8	f = mymalloc (3);
	9	f[2] = '2';
	10	free (f);
	11	}