1 # include <stdio.h>
2 
main(int argc,char ** argv)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 }
19