test/tainted/tainted3.c~

   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 }