1 extern void checkUntainted (char **s) /*@requires untainted *s@*/;
3 typedef /*@tainted@*/ char *charpt;
4 extern void checkTainted (charpt *s) ; /* requires tainted *s doesn't work because of implicit annotation! */
6 void test (/*@tainted@*/ char *def)
9 checkUntainted (&def); /* error */