void monitor_print_filename(Monitor *mon, const char *filename);
void monitor_flush(Monitor *mon);
int monitor_set_cpu(int cpu_index);
void monitor_print_filename(Monitor *mon, const char *filename);
void monitor_flush(Monitor *mon);
int monitor_set_cpu(int cpu_index);