From ee5c3774806f86caab8e5c3fe45ed19512f49819 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 12 Feb 2020 10:22:59 +0100
Subject: [exn] Keep information from multiple extra exn handlers

This fixes #11547 ; note that it is hard to register such handlers in
the `Summary` due to layering issues; there are potential anomalies here
depending on how plugins do register their data structures.
---
 lib/cErrors.ml  | 15 ++++++---------
 lib/cErrors.mli |  2 +-
 2 files changed, 7 insertions(+), 10 deletions(-)

(limited to 'lib')

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 323dc8c1a4..a23cf3aaf1 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -79,7 +79,7 @@ let is_anomaly = function
 (** Printing of additional error info, from Exninfo *)
 let additional_error_info_handler = ref []
 
-let register_additional_error_info (f : Exninfo.info -> (Pp.t option Loc.located) option) =
+let register_additional_error_info (f : Exninfo.info -> (Pp.t Loc.located) option) =
   additional_error_info_handler := f :: !additional_error_info_handler
 
 (** [print_gen] is a general exception printer which tries successively
@@ -93,18 +93,15 @@ let rec print_gen ~anomaly ~extra_msg stk e =
   | h::stk' ->
     match h e with
     | Some err_msg ->
-      Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg
+      extra_msg ++ err_msg
     | None ->
       print_gen ~anomaly ~extra_msg stk' e
 
 let print_gen ~anomaly (e, info) =
-  let extra_info =
-    try CList.find_map (fun f -> Some (f info)) !additional_error_info_handler
-    with Not_found -> None
-  in
-  let extra_msg = match extra_info with
-    | None -> None
-    | Some (loc, msg) -> msg
+  let extra_msg =
+    CList.map_filter (fun f -> f info) !additional_error_info_handler
+    (* Location info in the handler is ignored *)
+    |> List.map snd |> Pp.seq
   in
   try
     print_gen ~anomaly ~extra_msg !handle_stack e
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 1660a00244..42e3975b72 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -75,5 +75,5 @@ val noncritical : exn -> bool
    exceptions. This method is fragile and should be considered
    deprecated *)
 val register_additional_error_info
-  :  (Exninfo.info -> (Pp.t option Loc.located) option)
+  :  (Exninfo.info -> Pp.t Loc.located option)
   -> unit
-- 
cgit v1.2.3