From 1badb1e51560be89951fff0cd04cdc59fcf4b1f3 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 12 Oct 2020 22:51:24 +0100
Subject: Support C coverage when sail_exit is used

---
 src/jib/c_backend.ml | 32 +++++++++++++++++++++-----------
 1 file changed, 21 insertions(+), 11 deletions(-)

(limited to 'src')

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)
-- 
cgit v1.2.3