From ef15d96e0fa957ce6962d74fba68d1150f3a9519 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 23 Nov 2021 09:33:50 +0100
Subject: [PATCH] [eacsl] improve error messaging through phases
---
src/plugins/e-acsl/src/analyses/typing.ml | 14 +++++++++-----
src/plugins/e-acsl/src/code_generator/quantif.ml | 1 +
src/plugins/e-acsl/src/libraries/error.ml | 8 ++++++--
src/plugins/e-acsl/src/libraries/error.mli | 11 ++++++++---
4 files changed, 24 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 18ebf2bfe89..9520deba969 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -882,6 +882,7 @@ and type_predicate ~lenv p =
"preprocessing of quantified predicate"
Bound_variables.get_preprocessed_quantifier
p
+ Printer.pp_predicate
in
let guards =
List.map
@@ -938,9 +939,9 @@ let unsafe_set t ?ctx ~lenv ty =
(******************************************************************************)
let get_number_ty ~lenv t =
- (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t).ty
+ (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term).ty
let get_integer_op ~lenv t =
- (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t).op
+ (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term).op
let get_integer_op_of_predicate ~lenv p = (type_predicate ~lenv p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
@@ -956,15 +957,18 @@ let extract_typ t ty =
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
let get_typ ~lenv t =
- let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
+ let info =
+ Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
extract_typ t info.ty
let get_op ~lenv t =
- let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
+ let info =
+ Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
extract_typ t info.op
let get_cast ~lenv t =
- let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
+ let info =
+ Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t Printer.pp_term in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 2a5e0a68ade..ee06ec1a361 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -71,6 +71,7 @@ let convert kf env loc ~is_forall quantif =
"preprocessing of quantified predicate"
Bound_variables.get_preprocessed_quantifier
quantif
+ Printer.pp_predicate
in
match has_empty_quantif_with_false_negative bound_vars, is_forall with
| true, true ->
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 6062ebdf0d6..795d4ec294c 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -79,13 +79,17 @@ let handle f x = generic_handle f x x
type 'a or_error = Res of 'a | Err of exn
-let retrieve_preprocessing analyse_name getter parameter =
+let retrieve_preprocessing analyse_name getter parameter pp =
try
match getter parameter with
| Res res -> res
| Err exn -> raise exn
with Not_memoized ->
- Options.fatal "%s was not performed on construct" analyse_name
+ Options.fatal
+ "%s was not performed on construct %a"
+ analyse_name
+ pp
+ parameter
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 9dcc0355b61..36224e573ca 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -59,10 +59,15 @@ val nb_not_yet: unit -> int
val print_not_yet: string -> unit
(** Print the "not yet" message without raising an exception. *)
-val retrieve_preprocessing: string -> ('a -> 'b or_error) -> 'a -> 'b
+val retrieve_preprocessing:
+ string ->
+ ('a -> 'b or_error) ->
+ 'a ->
+ (Format.formatter -> 'a -> unit) ->
+ 'b
(** Retrieve the result of a preprocessing phase, which possibly failed.
- The [string] argument is used to display a message in case the preprocessing
- phase did not compute the required result. *)
+ The [string] argument and the formatter are used to display a message in
+ case the preprocessing phase did not compute the required result. *)
(*
Local Variables:
--
GitLab