escript/src/blocktimer.h

#include <stdio.h>
#include <search.h>

/* Enable the block timer (or remove this and use -DBLOCKTIMER) */
# define BLOCKTIMER

# define NUM_TIMERS 1024

void blocktimer_initialize();
void blocktimer_increment(char *name, double start_time);
int blocktimer_getOrCreateTimerId(char *name);
void blocktimer_reportSortByName();
void blocktimer_reportSortByTime();
double blocktimer_time();

1	#include <stdio.h>
2	#include <search.h>
3
4	/* Enable the block timer (or remove this and use -DBLOCKTIMER) */
5	# define BLOCKTIMER
6
7	# define NUM_TIMERS 1024
8
9	void blocktimer_initialize();
10	void blocktimer_increment(char *name, double start_time);
11	int blocktimer_getOrCreateTimerId(char *name);
12	void blocktimer_reportSortByName();
13	void blocktimer_reportSortByTime();
14	double blocktimer_time();
15