1 typedef /*@abstract@*/ /*@null@*/ char *mstring;
3 static mstring mstring_createNew (int x) ;
5 mstring mstring_space1 (void)
7 mstring m = mstring_createNew (1);
9 /* error, since m could be NULL */
10 *m = ' '; *(m + 1) = '\0';
14 static /*@notnull@*/ mstring mstring_createNewNN (int x) ;
16 mstring mstring_space2 (void)
18 mstring m = mstring_createNewNN (1);
20 /* no error, because of notnull annotation */
21 *m = ' '; *(m + 1) = '\0';