test/arraylit.c

   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 }