extern bool flags_isModeName (cstring p_s) /*@*/ ;
extern /*@only@*/ cstring describeModes (void) /*@modifies g_messagestream@*/ ;
+extern /*@only@*/ cstring describeMode (/*@observer@*/ cstring mode) /*@*/ ;
extern void summarizeErrors (void) /*@modifies g_messagestream@*/ ;
extern bool flagcode_isNameChecksFlag (flagcode p_f) /*@*/ ;