[splint.git] / test / metastate / tainted4.c

extern void checkUntainted (char **s) /*@requires untainted *s@*/;
extern void checkTainted (char **s) /*@requires tainted *s@*/;

void test (/*@tainted@*/ char *def)
{
  checkTainted (&def);
  checkUntainted (&def); /* error */
}
Commit	Line	Data
80ee600a	1	extern void checkUntainted (char *s) /@requires untainted s@/;
	2	extern void checkTainted (char *s) /@requires tainted s@/;
	3
	4	void test (/@tainted@/ char *def)
	5	{
	6	checkTainted (&def);
	7	checkUntainted (&def); /* error */
	8	}