[splint.git] / test / manual / mstringnn.c

typedef /*@abstract@*/ /*@null@*/ char *mstring;

static mstring mstring_createNew (int x) ;

mstring mstring_space1 (void)
{
  mstring m = mstring_createNew (1);

  /* error, since m could be NULL */
  *m = ' '; *(m + 1) = '\0';
  return m;
}

static /*@notnull@*/ mstring mstring_createNewNN (int x) ;

mstring mstring_space2 (void)
{
  mstring m = mstring_createNewNN (1);

  /* no error, because of notnull annotation */
  *m = ' '; *(m + 1) = '\0';
  return m;
}
Commit	Line	Data
77970e15	1	typedef /@abstract@/ /@null@/ char *mstring;
	2
	3	static mstring mstring_createNew (int x) ;
	4
	5	mstring mstring_space1 (void)
	6	{
	7	mstring m = mstring_createNew (1);
	8
	9	/* error, since m could be NULL */
	10	m = ' '; (m + 1) = '\0';
	11	return m;
	12	}
	13
	14	static /@notnull@/ mstring mstring_createNewNN (int x) ;
	15
	16	mstring mstring_space2 (void)
	17	{
	18	mstring m = mstring_createNewNN (1);
	19
	20	/* no error, because of notnull annotation */
	21	m = ' '; (m + 1) = '\0';
	22	return m;
	23	}