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@*/;
6 void test2 (char **def) /*@requires untainted *def@*/
9 checkTainted (def); /* error */
12 void test (char *def2) /*@requires untainted def2@*/
14 checkUntainted1 (&def2);
15 checkTainted1 (&def2); /* error */