Support C coverage when sail_exit is used

2 files changed, 24 insertions, 11 deletions

diff --git a/lib/rts.c b/lib/rts.c
index 16a2eca4..c1da2097 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -10,9 +10,12 @@ static uint64_t g_elf_entry;
 uint64_t g_cycle_count = 0;
 static uint64_t g_cycle_limit;
 
+extern void model_pre_exit();
+
 unit sail_exit(unit u)
 {
   fprintf(stderr, "[Sail] Exiting after %" PRIu64 " cycles\n", g_cycle_count);
+  model_pre_exit();
   exit(EXIT_SUCCESS);
   return UNIT;
 }
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)