[eacsl] Add phase information to error messages

src/plugins/e-acsl/E_ACSL.mli

@@ -24,9 +24,13 @@
 
 open Cil_types
 
+module Options: sig
+  type category
+end
+
 module Error: sig
-  exception Typing_error of string
-  exception Not_yet of string
+  exception Typing_error of Options.category option * string
+  exception Not_yet of Options.category option * string
 end
 
 module Translate_terms: sig

src/plugins/e-acsl/src/libraries/error.ml

@@ -22,14 +22,39 @@
 
 open Error_types
 
-exception Typing_error of string
-let untypable s = raise (Typing_error s)
+module Exn_impl = struct
+  exception Typing_error of Options.category option * string
+  exception Not_yet of Options.category option * string
+  exception Not_memoized of Options.category option
+end
 
-exception Not_yet of string
-let not_yet s = raise (Not_yet s)
+module type Exn = module type of Exn_impl
 
-exception Not_memoized
-let not_memoized () = raise Not_memoized
+module type S = sig
+  include Exn
+  val make_untypable: string -> exn
+  val make_not_yet: string -> exn
+  val make_not_memoized: unit -> exn
+  val untypable: string -> 'a
+  val not_yet: string -> 'a
+  val not_memoized: unit -> 'a
+  val print_not_yet: string -> unit
+  val handle: ('a -> 'a) -> 'a -> 'a
+  val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
+  val nb_untypable: unit -> int
+  val nb_not_yet: unit -> int
+  val retrieve_preprocessing:
+    string ->
+    ('a -> 'b or_error) ->
+    'a ->
+    (Format.formatter -> 'a -> unit) ->
+    'b
+  val pp_or_error:
+    (Format.formatter -> 'a -> unit) ->
+    Format.formatter ->
+    'a or_error ->
+    unit
+end
 
 module Nb_typing =
   State_builder.Ref
@@ -40,8 +65,6 @@ module Nb_typing =
       let dependencies = [ Ast.self ]
     end)
 
-let nb_untypable = Nb_typing.get
-
 module Nb_not_yet =
   State_builder.Ref
     (Datatype.Int)
@@ -51,46 +74,85 @@ module Nb_not_yet =
       let dependencies = [ Ast.self ]
     end)
 
-let nb_not_yet = Nb_not_yet.get
-
-let print_not_yet msg =
-  let msg =
-    Format.sprintf "@[E-ACSL construct@ `%s'@ is not yet supported.@]" msg
-  in
-  Options.warning ~once:true ~current:true "@[%s@ Ignoring annotation.@]" msg;
-  Nb_not_yet.set (Nb_not_yet.get () + 1)
-
-let generic_handle f res x =
-  try
-    f x
-  with
-  | Typing_error s ->
-    let msg = Format.sprintf "@[invalid E-ACSL construct@ `%s'.@]" s in
-    Options.warning ~once:true ~current:true "@[%s@ Ignoring annotation.@]" msg;
-    Nb_typing.set (Nb_typing.get () + 1);
-    res
-  | Not_yet s ->
-    print_not_yet s;
-    res
-
-let handle f x = generic_handle f x x
-
-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 %a"
-      analyse_name
-      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)
+module Make_with_opt(P: sig val phase:Options.category option end): S = struct
+  include Exn_impl
+
+  let make_untypable msg = Typing_error (P.phase, msg)
+  let make_not_yet msg = Not_yet (P.phase, msg)
+  let make_not_memoized () = Not_memoized P.phase
+
+  let untypable msg = raise (make_untypable msg)
+  let not_yet msg = raise (make_not_yet msg)
+  let not_memoized () = raise (make_not_memoized ())
+
+  let nb_untypable = Nb_typing.get
+  let nb_not_yet = Nb_not_yet.get
+
+  let pp_phase fmt phase =
+    match phase with
+    | Some phase ->
+      if Options.verbose_atleast 2 then
+        Format.fprintf fmt "@[@ in phase `%a'@]" Options.pp_category phase
+    | None -> ()
+
+  let do_print_not_yet phase msg =
+    let msg =
+      Format.asprintf
+        "@[E-ACSL construct@ `%s'@ is not yet supported%a.@]"
+        msg
+        pp_phase phase
+    in
+    Options.warning
+      ~once:true ~current:true
+      "@[%s@ Ignoring annotation.@]" msg;
+    Nb_not_yet.set (Nb_not_yet.get () + 1)
+
+  let print_not_yet msg =
+    do_print_not_yet P.phase msg
+
+  let generic_handle f res x =
+    try
+      f x
+    with
+    | Typing_error (phase, s) ->
+      let msg =
+        Format.asprintf "@[invalid E-ACSL construct@ `%s'%a.@]"
+          s
+          pp_phase phase
+      in
+      Options.warning
+        ~once:true ~current:true
+        "@[%s@ Ignoring annotation.@]" msg;
+      Nb_typing.set (Nb_typing.get () + 1);
+      res
+    | Not_yet (phase, s) ->
+      do_print_not_yet phase s;
+      res
+
+  let handle f x = generic_handle f x x
+
+  let retrieve_preprocessing analyse_name getter parameter pp =
+    try
+      match getter parameter with
+      | Res res -> res
+      | Err exn -> raise exn
+    with Not_memoized phase ->
+      Options.fatal
+        "@[%s was not performed on construct %a%a@]"
+        analyse_name
+        pp parameter
+        pp_phase phase
+
+  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)
+end
+
+module Make(P: sig val phase:Options.category end): S =
+  Make_with_opt(struct let phase = Some P.phase end)
+
+include Make_with_opt(struct let phase = None end)
 
 (*
 Local Variables:

src/plugins/e-acsl/src/libraries/error.mli

@@ -23,57 +23,89 @@
 (** Handling errors. *)
 open Error_types
 
-exception Typing_error of string
-exception Not_yet of string
-exception Not_memoized
-
-val untypable: string -> 'a
-(** Type error built from the given argument. *)
-
-val not_yet: string -> 'a
-(** Not_yet_implemented error built from the given argument. *)
-
-val not_memoized : unit -> 'a
-(** @raise Not_memoized  when asking the preprocessed form of something that
-    was not preprocessed *)
-
-val handle: ('a -> 'a) -> 'a -> 'a
-(** Run the closure with the given argument and handle potential errors.
-    Return the provide argument in case of errors. *)
-
-val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
-(** Run the closure with the given argument and handle potential errors.
-    Return the additional argument in case of errors. *)
-
-val nb_untypable: unit -> int
-(** Number of untypable annotations. *)
-
-val nb_not_yet: unit -> int
-(** Number of not-yet-supported annotations. *)
-
-val print_not_yet: string -> unit
-(** Print the "not yet" message without raising an exception. *)
-
-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 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]. *)
+(** Internal module holding the exception of [Error].
+
+    The module is included into [S] later and should not be used directly.
+    However we need to have a separate module for the exception so that every
+    exception built by [Make] is the exact same type. *)
+module type Exn = sig
+  exception Typing_error of Options.category option * string
+  (** Typing error where the first element is the phase where the error occured
+      and the second element is the error message. *)
+
+  exception Not_yet of Options.category option * string
+  (** "Not yet supported" error where the first element is the phase where the
+      error occured and the second element is the error message. *)
+
+  exception Not_memoized of Options.category option
+  (** "Not memoized" error with the phase where the error occured. *)
+end
+
+module type S = sig
+  include Exn
+
+  val make_untypable: string -> exn
+  (** Make a [Typing_error] exception with the given message. *)
+
+  val make_not_yet: string -> exn
+  (** Make a [Not_yet] exception with the given message. *)
+
+  val make_not_memoized: unit -> exn
+  (** Make a [Not_memoized] exception with the given message. *)
+
+  val untypable: string -> 'a
+  (** @raise Typing_error with the given message. *)
+
+  val not_yet: string -> 'a
+  (** @raise Not_yet with the given message. *)
+
+  val not_memoized: unit -> 'a
+  (** @raise Not_memoized *)
+
+  val print_not_yet: string -> unit
+  (** Print the "not yet supported" message without raising an exception. *)
+
+  val handle: ('a -> 'a) -> 'a -> 'a
+  (** Run the closure with the given argument and handle potential errors.
+      Return the provide argument in case of errors. *)
+
+  val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
+  (** Run the closure with the given argument and handle potential errors.
+      Return the additional argument in case of errors. *)
+
+  val nb_untypable: unit -> int
+  (** Number of untypable annotations. *)
+
+  val nb_not_yet: unit -> int
+  (** Number of not-yet-supported annotations. *)
+
+  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 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]. *)
+end
+
+(** Functor to build an [Error] module for a given [phase]. *)
+module Make(P: sig val phase:Options.category end): S
+
+(** The [Error] module implements [Error.S] with no phase. *)
+include S
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
 End:
 *)