[splint.git] / test / tainted / tainted5.c~

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

void test (char *def) /*@requires untainted def@*/ 
{
  checkUntainted (&def); 
  checkTainted (&def); /* error */
}

void test2 (char **def) /*@requires untainted *def@*/ 
{
  checkUntainted (def); 
  checkTainted (def); /* error */
}
Commit	Line	Data
98ed3b22	1	extern void checkUntainted (char *s) /@requires untainted s@/;
	2	extern void checkTainted (char *s) /@requires tainted s@/;
	3
	4	void test (char def) /@requires untainted def@*/
	5	{
	6	checkUntainted (&def);
	7	checkTainted (&def); /* error */
	8	}
	9
	10	void test2 (char *def) /@requires untainted def@/
	11	{
	12	checkUntainted (def);
	13	checkTainted (def); /* error */
	14	}