test/tainted/tainted4.c~

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