From d48af10f5a2ef06b518e86398d504706e4995e09 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 Apr 2020 09:05:26 +0200 Subject: now use COMPCERT_PROFILING_DATA and don't print stuff --- runtime/c/write_profiling_table.c | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'runtime') diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 60bae3d7..0ce7a948 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -1,5 +1,6 @@ #include #include +#include #include typedef uint8_t md5_hash[16]; @@ -25,8 +26,15 @@ void _compcert_write_profiling_table(unsigned int nr_items, md5_hash id_table[], condition_counters counter_table[]) { errno = 0; + + const char *filename = getenv("COMPCERT_PROFILING_DATA"); + if (filename) { + if (!*filename) return; + } else { + filename = "compcert_profiling.dat"; + } - FILE *fp = fopen("compcert_profiling.dat", "a"); + FILE *fp = fopen(filename, "a"); //fprintf(stderr, "successfully opened profiling file\n"); if (fp == NULL) { perror("open CompCert profiling data for writing"); @@ -46,5 +54,5 @@ void _compcert_write_profiling_table(unsigned int nr_items, perror("write CompCert profiling data"); return; } - fprintf(stderr, "write CompCert profiling data: no error\n"); + // fprintf(stderr, "write CompCert profiling data: no error\n"); } -- cgit