[eacsl] improve error messaging through phases

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
 

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 ->

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:

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: