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