[splint.git] / test / metastate / tainted3.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	}