diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 71b050fa887e0297a3119eb85e8e3f7ac2a95f15..6293096f839786cc180abde533f17be0954c8c60 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -91,6 +91,11 @@ let retrieve_preprocessing analyse_name getter parameter pp =
       pp
       parameter
 
+let pp_or_error pp fmt a_or_error =
+  match a_or_error with
+  | Res a -> Format.fprintf fmt "@[%a@]" pp a
+  | Err err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
+
 (*
 Local Variables:
 compile-command: "make"
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 2f8b05d1c7d91c24987bfe3dd954dcaff002e05d..9d35c516a3367e36ba4ffd9f57adea69ac1cd405 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -68,6 +68,14 @@ val retrieve_preprocessing:
     The [string] argument and the formatter are used to display a message in
     case the preprocessing phase did not compute the required result. *)
 
+val pp_or_error:
+  (Format.formatter -> 'a -> unit) ->
+  Format.formatter ->
+  'a or_error ->
+  unit
+(** [pp_or_error pp] where [pp] is a formatter for ['a] returns a formatter for
+    ['a or_error]. *)
+
 (*
 Local Variables:
 compile-command: "make"