]>
Commit | Line | Data |
---|---|---|
37ae0b5e | 1 | # include <stdio.h> |
2 | ||
3 | int main (/*@unused@*/ int argc, /*@unused@*/ char **argv) /*@*/ | |
4 | { | |
5 | /*@observer@*/ char *unmodstr = "unmodifiable string"; | |
6 | /*@exposed@*/ char modstr[20] = "modifiable string"; | |
7 | /*@unused@*/ char modstr1[5] = "12345"; /* not enough space */ | |
8 | /*@unused@*/ char modstr2[6] = "12345"; | |
9 | /*@unused@*/ char modstr3[7] = "12345"; /* if +stringliteralsmaller */ | |
10 | ||
11 | modstr1 = modstr; | |
12 | ||
13 | unmodstr[0] = 'U'; /* line 6; not OK */ | |
14 | modstr[0] = 'M'; /* line 7; OK */ | |
15 | ||
16 | fprintf (stderr, "mod: %s mod1: %s", modstr, modstr1); | |
17 | return 0; | |
18 | } |