extern /*@notnull@*/ /*@only@*/ char *mstring_createEmpty (void) /*@*/ ;
extern void mstring_free (/*@out@*/ /*@only@*/ /*@null@*/ char *p_s);
extern /*@notnull@*/ /*@only@*/ char *mstring_createEmpty (void) /*@*/ ;
extern void mstring_free (/*@out@*/ /*@only@*/ /*@null@*/ char *p_s);