diff options
| author | Brian Campbell | 2020-10-12 22:51:24 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-10-14 22:46:27 +0100 |
| commit | 1badb1e51560be89951fff0cd04cdc59fcf4b1f3 (patch) | |
| tree | 435b868aa6e003b170be6736916534475efe37f6 /src/jib | |
| parent | 8b6a4923645c733af26d0650617844200996b350 (diff) | |
Support C coverage when sail_exit is used
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 32 |
1 files changed, 21 insertions, 11 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 2fe21d93..88b01d87 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2310,23 +2310,32 @@ let compile_ast env output_chan c_includes ast = @ [ "}" ] )) in + let model_pre_exit = + [ "void model_pre_exit()"; + "{" ] + @ (if Util.is_some !opt_branch_coverage then + [ " if (sail_coverage_exit() != 0) {"; + " fprintf(stderr, \"Could not write coverage information\\n\");"; + " exit(EXIT_FAILURE);"; + " }"; + "}" ] + else + ["}"] + ) + |> List.map string + |> separate hardline + in + let model_default_main = ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (static ()); "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); - " model_fini();" ] - @ (if Util.is_some !opt_branch_coverage then - [ " if (sail_coverage_exit() != 0) {"; - " fprintf(stderr, \"Could not write coverage information\\n\");"; - " exit(EXIT_FAILURE);"; - " }" ] - else - [] - ) - @ [ " return EXIT_SUCCESS;"; - "}" ]) + " model_fini();"; + " model_pre_exit();"; + " return EXIT_SUCCESS;"; + "}" ]) |> List.map string |> separate hardline in @@ -2344,6 +2353,7 @@ let compile_ast env output_chan c_includes ast = ^^ (if not !opt_no_rts then model_init ^^ hlhl ^^ model_fini ^^ hlhl + ^^ model_pre_exit ^^ hlhl ^^ model_default_main ^^ hlhl else empty) |