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 
test2(char ** def)6 void test2 (char **def) /*@requires untainted *def@*/
7 {
8   checkUntainted (def);
9   checkTainted (def); /* error */
10 }
11 
test(char * def2)12 void test (char *def2) /*@requires untainted def2@*/
13 {
14   checkUntainted1 (&def2);
15   checkTainted1 (&def2); /* error */
16 }
17 
18