[Eva] Runs audit-prepare only once as a normal exit hook.

src/kernel_services/ast_queries/file.ml

@@ -1666,9 +1666,8 @@ let print_all_sources out all_sources_tbl =
     in
     try Json.merge_object out json
     with Json.CannotMerge _ ->
-      Kernel.abort "%s already computed; it should be set by itself, \
-                    after the last '-then' in the command line."
-        Kernel.AuditPrepare.option_name
+      Kernel.failure "%s: error when writing json file %a."
+        Kernel.AuditPrepare.option_name Filepath.Normalized.pretty out
   end
 
 let compute_sources_table cpp_commands =
@@ -1756,6 +1755,21 @@ let print_and_exit cpp_commands =
   List.iter (fun (_f, ocmd) -> Option.iter print_cpp_cmd ocmd) cpp_commands;
   raise Cmdline.Exit
 
+let prepare_audit () =
+  let audit_path = Kernel.AuditPrepare.get () in
+  if not (Filepath.Normalized.is_empty audit_path) then
+    let files = Files.get () in (* Allow pre-registration of prologue files *)
+    let cpp_commands = List.map (fun f -> (f, build_cpp_cmd f)) files in
+    let all_sources_tbl = compute_sources_table cpp_commands in
+    print_all_sources audit_path all_sources_tbl;
+    (* This is normally done by another hook at normal exit, but it is done
+       before our hook, so we need to redo it. *)
+    if not (Filepath.Normalized.is_special_stdout audit_path) then
+      Kernel.feedback "Audit: sources list written to: %a@."
+        Filepath.Normalized.pretty audit_path
+
+let () = Cmdline.at_normal_exit prepare_audit
+
 let prepare_from_c_files () =
   init_cil ();
   let files = Files.get () in (* Allow pre-registration of prolog files *)
@@ -1767,14 +1781,6 @@ let prepare_from_c_files () =
     let expected_hashes = source_hashes_of_json audit_check_path in
     check_source_hashes expected_hashes all_sources_tbl
   end;
-  let audit_path = Kernel.AuditPrepare.get () in
-  if not (Filepath.Normalized.is_empty audit_path) then begin
-    let all_sources_tbl = compute_sources_table cpp_commands in
-    print_all_sources audit_path all_sources_tbl;
-    if not (Filepath.Normalized.is_special_stdout audit_path) then
-      Kernel.feedback "Audit: sources list written to: %a@."
-        Filepath.Normalized.pretty audit_path;
-  end;
   let cil, cabs_files = files_to_cabs_cil files cpp_commands in
   prepare_cil_file cil;
   (* prepare_cil_file may call syntactic transformers, that will ultimately

src/plugins/value/engine/analysis.ml

@@ -175,8 +175,6 @@ let force_compute () =
   Value_parameters.configure_precision ();
   if not (Kernel.AuditCheck.is_empty ()) then
     Eva_audit.check_configuration (Kernel.AuditCheck.get ());
-  if not (Kernel.AuditPrepare.is_empty ()) then
-    Eva_audit.print_configuration (Kernel.AuditPrepare.get ());
   let kf, lib_entry = Globals.entry_point () in
   reset_analyzer ();
   let module Analyzer = (val snd !ref_analyzer) in

src/plugins/value/utils/eva_audit.ml

@@ -148,8 +148,16 @@ let print_configuration path =
   try
     print_correctness_parameters path;
     print_warning_status path "Kernel" (module Kernel);
-    print_warning_status path "Eva" (module Value_parameters)
+    print_warning_status path "Eva" (module Value_parameters);
+    if not (Filepath.Normalized.is_special_stdout path) then
+      Value_parameters.feedback "Audit: eva configuration written to: %a"
+        Filepath.Normalized.pretty path;
   with Json.CannotMerge _ ->
-    Kernel.abort "%s already computed; it should be set by itself, \
-                  after the last '-then' in the command line."
-      Kernel.AuditPrepare.option_name
+    Kernel.failure "%s: error when writing json file %a."
+      Kernel.AuditPrepare.option_name Filepath.Normalized.pretty path
+
+let prepare_audit () =
+  if not (Kernel.AuditPrepare.is_empty ()) then
+    print_configuration (Kernel.AuditPrepare.get ())
+
+let () = Cmdline.at_normal_exit prepare_audit

tests/misc/oracle/audit.res.oracle

@@ -5,7 +5,6 @@
 [kernel:audit] Warning: 
   missing files:
   tests/misc/non_existing_file.h
-[kernel] Audit: sources list written to: tests/misc/result/audit-out.json
 [kernel] Parsing tests/misc/audit.c (with preprocessing)
 [kernel:parser:decimal-float] tests/misc/audit.c:10: Warning: 
   Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1.
@@ -31,4 +30,6 @@
     f
 [inout] Inputs for function main:
     \nothing
+[kernel] Audit: sources list written to: tests/misc/result/audit-out.json
+[eva] Audit: eva configuration written to: tests/misc/result/audit-out.json
 [kernel] Wrote: tests/misc/result/audit-out.json