From 647a926c3ab3a915762ac720347ce941c1f62af0 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 14 Jan 2022 13:36:26 +0100
Subject: [PATCH] [eacsl] Pretty-printing function for Error.or_error
---
src/plugins/e-acsl/src/libraries/error.ml | 5 +++++
src/plugins/e-acsl/src/libraries/error.mli | 8 ++++++++
2 files changed, 13 insertions(+)
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 71b050fa887..6293096f839 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 2f8b05d1c7d..9d35c516a33 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"
--
GitLab