extern /*@observer@*/ cstring flagcode_unparse (flagcode p_code) /*@*/ ;
extern int flagcode_valueIndex (flagcode p_f) /*@*/ ;
extern int flagcode_stringIndex (flagcode p_f) /*@*/ ;
extern /*@observer@*/ cstring flagcode_unparse (flagcode p_code) /*@*/ ;
extern int flagcode_valueIndex (flagcode p_f) /*@*/ ;
extern int flagcode_stringIndex (flagcode p_f) /*@*/ ;