test/manual/mstringnn.c

   1 typedef /*@abstract@*/ /*@null@*/ char *mstring;
   2
   3 static mstring mstring_createNew (int x) ;
   4
   5 mstring mstring_space1 (void)
   6 {
   7   mstring m = mstring_createNew (1);
   8
   9   /* error, since m could be NULL */
  10   *m = ' '; *(m + 1) = '\0';
  11   return m;
  12 }
  13
  14 static /*@notnull@*/ mstring mstring_createNewNN (int x) ;
  15
  16 mstring mstring_space2 (void)
  17 {
  18   mstring m = mstring_createNewNN (1);
  19
  20   /* no error, because of notnull annotation */
  21   *m = ' '; *(m + 1) = '\0';
  22   return m;
  23 }