diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index e8621a40599add149915ad65da9a76ab815eb93a..d99085bdc92853a63da61452820ea4607706a0b4 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -1664,7 +1664,11 @@ let print_all_sources out all_sources_tbl = `Assoc (List.map (fun (f, hash) -> f, `String hash) sorted_elems) )] in - Json.merge_object out json + 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 end let compute_sources_table cpp_commands = @@ -1766,14 +1770,7 @@ let prepare_from_c_files () = 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 - begin - try - print_all_sources audit_path all_sources_tbl - 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 - end; + 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; diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml index 5862fe01dff95e708092053acf02bb6436a6047b..33c7c3687c564d51e19b87ceca850b0687a751a2 100644 --- a/src/plugins/value/engine/analysis.ml +++ b/src/plugins/value/engine/analysis.ml @@ -176,14 +176,7 @@ let force_compute () = if not (Kernel.AuditCheck.is_empty ()) then Eva_audit.check_configuration (Kernel.AuditCheck.get ()); if not (Kernel.AuditPrepare.is_empty ()) then - begin - try - Eva_audit.print_configuration (Kernel.AuditPrepare.get ()); - 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 - end; + 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 diff --git a/src/plugins/value/utils/eva_audit.ml b/src/plugins/value/utils/eva_audit.ml index c376dfe5fcabaafd1896520d4fb1cf48768f005e..507125082c39fa8b5a7a0263a67e5c753ff3871c 100644 --- a/src/plugins/value/utils/eva_audit.ml +++ b/src/plugins/value/utils/eva_audit.ml @@ -145,6 +145,11 @@ let check_configuration path = Filepath.Normalized.pretty path msg let print_configuration path = - print_correctness_parameters path; - print_warning_status path "Kernel" (module Kernel); - print_warning_status path "Eva" (module Value_parameters) + try + print_correctness_parameters path; + print_warning_status path "Kernel" (module Kernel); + print_warning_status path "Eva" (module Value_parameters) + 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