]>
Commit | Line | Data |
---|---|---|
1 | char *taintme (char *s) | |
2 | /*@ensures result:taintedness = s:taintedness@*/ | |
3 | { | |
4 | char *res = (char *) malloc (sizeof (*res) * strlen (s)); | |
5 | assert (res != NULL); | |
6 | strcpy (res, s); | |
7 | return res; | |
8 | } | |
9 | ||
10 | void safecall (/*@untainted@*/ char *s) | |
11 | { | |
12 | (void) system (taintme (s)); /* okay */ | |
13 | } | |
14 | ||
15 | void dangerouscall (/*@tainted@*/ char *s) | |
16 | { | |
17 | (void) system (taintme (s)); /* error */ | |
18 | } |