extern bool flags_isModeName (cstring p_s) /*@*/ ;
extern /*@only@*/ cstring describeModes (void) /*@modifies g_messagestream@*/ ;
extern bool flags_isModeName (cstring p_s) /*@*/ ;
extern /*@only@*/ cstring describeModes (void) /*@modifies g_messagestream@*/ ;