/*@only@*/ /*@open@*/ FILE *g_msgstream;