]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
2 | ** checks read-only strings | |
3 | */ | |
4 | ||
5 | char f1 (char *x) | |
6 | { | |
7 | return *x; | |
8 | } | |
9 | ||
10 | char f2 (char *x) /*@modifies *x;@*/ | |
11 | { | |
12 | *x = 'a'; | |
13 | return *x; | |
14 | } | |
15 | ||
16 | void f3 (/*@only@*/ char *x) | |
17 | { | |
18 | free (x); | |
19 | } | |
20 | ||
21 | void main (void) | |
22 | { | |
23 | (void) f1 ("hullo"); | |
24 | (void) f2 ("hullo"); | |
25 | f3 ("hullo"); | |
26 | } |