test/tainted/taintedx.c

   1 extern void checkUntainted (char **s) /*@requires untainted *s@*/;
   2 extern void checkUntainted1 (char **s) /*@requires untainted *s@*/;
   3 extern void checkTainted (char **s) /*@requires tainted *s@*/;
   4 extern void checkTainted1 (char **s) /*@requires tainted *s@*/;
   5
   6 void test2 (char **def) /*@requires untainted *def@*/
   7 {
   8   checkUntainted (def);
   9   checkTainted (def); /* error */
  10 }
  11
  12 void test (char *def2) /*@requires untainted def2@*/
  13 {
  14   checkUntainted1 (&def2);
  15   checkTainted1 (&def2); /* error */
  16 }
  17