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	ksteube	1314	#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