test/tainted/tainted5.c~

   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 }