]>
Commit | Line | Data |
---|---|---|
80ee600a | 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 |