diff --git a/lib/rts.c b/lib/rts.c index 7ddc7f2c8..88d598ae9 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -71,9 +71,6 @@ #include #include "sail.h" -#ifdef HAVE_COVERAGE -#include "sail_coverage.h" -#endif #include "rts.h" #include "elf.h" @@ -81,6 +78,8 @@ extern "C" { #endif +extern void sail_rts_set_coverage_file(char *output_file); + static uint64_t g_elf_entry; uint64_t g_cycle_count = 0; static uint64_t g_cycle_limit; @@ -726,11 +725,11 @@ int process_arguments(int argc, char *argv[]) break; case 'c': -#ifdef HAVE_COVERAGE - sail_set_coverage_file(optarg); -#else - fprintf(stderr, "Ignoring flag -c %s. Requires sail arg: -c_include sail_coverage.h\n", optarg); -#endif + if (&sail_rts_set_coverage_file) { + sail_rts_set_coverage_file(optarg); + } else { + fprintf(stderr, "Ignoring flag -c %s. Requires sail arg: -c_include sail_coverage.h\n", optarg); + } break; case 'v': diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index 7e10f4b59..c2f33a581 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -2005,11 +2005,19 @@ let compile_ast env effect_info output_chan c_includes ast = let docs = separate_map (hardline ^^ hardline) (codegen_def ctx) cdefs in + (* Generate a hook for the RTS to call if we have coverage enabled, so it can set the output file with an option. *) + let coverage_hook = + string "void sail_rts_set_coverage_file(char *output_file) { sail_set_coverage_file(output_file); }" + in + let no_coverage_hook = + string "void (*sail_rts_set_coverage_file)(char *) = NULL;" + in + let preamble = separate hardline ((if !opt_no_lib then [] else [string "#include \"sail.h\""]) @ (if !opt_no_rts then [] else [string "#include \"rts.h\""; string "#include \"elf.h\""]) - @ (if Option.is_some !opt_branch_coverage then [string "#include \"sail_coverage.h\""] else []) + @ (if Option.is_some !opt_branch_coverage then [string "#include \"sail_coverage.h\""; coverage_hook] else [no_coverage_hook]) @ List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes @ [string "#ifdef __cplusplus"; string "extern \"C\" {"; string "#endif"] ) diff --git a/test/sailcov/run_tests.py b/test/sailcov/run_tests.py index 3fdd98fbf..72c5de42b 100755 --- a/test/sailcov/run_tests.py +++ b/test/sailcov/run_tests.py @@ -39,7 +39,7 @@ def test_sailcov(): tests[filename] = os.fork() if tests[filename] == 0: step('{} -no_warn -no_memo_z3 -c -c_include sail_coverage.h -c_coverage {}.branches {} -o {}'.format(sail, basename, filename, basename)) - step('cc -DHAVE_COVERAGE {}.c {}/lib/*.c {}/lib/coverage/libsail_coverage.a -lgmp -lz -lpthread -ldl -I {}/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename)) + step('cc {}.c {}/lib/*.c {}/lib/coverage/libsail_coverage.a -lgmp -lz -lpthread -ldl -I {}/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename)) step('./{}.bin -c {}.taken'.format(basename, basename)) step('{} --all {}.branches --taken {}.taken {}'.format(sailcov, basename, basename, filename)) step('diff {}.html {}.expect'.format(basename, basename))