From 8cf44f7879b3aef188768591d884851b4d9fcd6c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 25 Aug 2020 14:46:13 +0200
Subject: [PATCH] [kernel] linting log
---
.Makefile.lint | 2 -
.../plugin_entry_points/log.ml | 59 ++++++++++---------
.../plugin_entry_points/log.mli | 50 ++++++++--------
3 files changed, 56 insertions(+), 55 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 80fb691a837..61f6b0eb4af 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -99,8 +99,6 @@ ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.ml
ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.mli
ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.ml
ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.mli
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/log.ml
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/log.mli
ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.ml
ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.mli
ML_LINT_KO+=src/kernel_services/visitors/visitor.ml
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index d40ae03aa1d..76093e208d0 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -71,7 +71,7 @@ type terminal = {
mutable delayed : (terminal -> unit) list ;
mutable output : string -> int -> int -> unit ;
(* Same as Format.make_formatter *)
- mutable flush : unit -> unit ;
+ mutable flush : unit -> unit ;
(* Same as Format.make_formatter *)
}
@@ -90,7 +90,7 @@ let is_ready t =
| Locked | DelayedLock -> false
| Ready -> true
-let term_clean t =
+let term_clean t =
if t.isatty && not t.clean then
begin
let u = "\r\027[K" in
@@ -126,7 +126,7 @@ let stdout = {
let clean () = term_clean stdout
-let set_output ?(isatty=false) output flush =
+let set_output ?(isatty=false) output flush =
set_terminal stdout isatty output flush
(* -------------------------------------------------------------------------- *)
@@ -204,7 +204,7 @@ let is_prefixed_event = function
let is_single_line text =
try ignore (String.index_from text 0 '\n') ; false
- with Not_found -> true
+ with Not_found -> true
let echo_firstline output text p q width =
let t = try String.index_from text p '\n' with Not_found -> succ q in
@@ -372,10 +372,13 @@ let () = Array.iteri
(* -------------------------------------------------------------------------- *)
let all_channels : (string,channelstate) Hashtbl.t = Hashtbl.create 31
-let default_emitters = Array.map (fun _ -> { listeners=[] ; echo=true }) all_kinds
+let default_emitters =
+ Array.map (fun _ -> { listeners=[] ; echo=true })
+ all_kinds
let new_emitters () =
- Array.map (fun e -> { listeners = e.listeners ; echo = e.echo }) default_emitters
+ Array.map (fun e -> { listeners = e.listeners ; echo = e.echo })
+ default_emitters
let get_emitters plugin =
try
@@ -498,7 +501,7 @@ let logwithfinal finally channel
Format.pp_print_newline fmt () ;
Format.pp_print_flush fmt () ;
let p,q = Rich_text.trim buffer in
- let output =
+ let output =
if p <= q then
let source = get_source current source in
let message = Rich_text.range buffer p q in
@@ -586,26 +589,26 @@ let deferred_raise ~fatal ~unreported event msg =
logwithfinal finally channel ?append ~kind:event.evt_kind msg
let treat_deferred_error () =
- match !deferred_exn with
- | DNo_exn -> ()
- | DWarn_as_error event ->
- let unreported = unreported_event event in
- let wkey =
- match event.evt_category with
- | None -> ""
- | Some s when s = unreported_error -> ""
- | Some s -> s
- in
- deferred_raise ~fatal:false ~unreported event
- "warning %s treated as deferred error." wkey
- | DError event ->
- let unreported = unreported_event event in
- deferred_raise ~fatal:false ~unreported event
- "Deferred error message was emitted during execution."
- | DFatal event ->
- let unreported = unreported_event event in
- deferred_raise ~fatal:true ~unreported event
- "Deferred internal error message was emitted during execution."
+ match !deferred_exn with
+ | DNo_exn -> ()
+ | DWarn_as_error event ->
+ let unreported = unreported_event event in
+ let wkey =
+ match event.evt_category with
+ | None -> ""
+ | Some s when s = unreported_error -> ""
+ | Some s -> s
+ in
+ deferred_raise ~fatal:false ~unreported event
+ "warning %s treated as deferred error." wkey
+ | DError event ->
+ let unreported = unreported_event event in
+ deferred_raise ~fatal:false ~unreported event
+ "Deferred error message was emitted during execution."
+ | DFatal event ->
+ let unreported = unreported_event event in
+ deferred_raise ~fatal:true ~unreported event
+ "Deferred internal error message was emitted during execution."
(* -------------------------------------------------------------------------- *)
(* --- Messages Interface --- *)
@@ -1242,7 +1245,7 @@ struct
with error ->
unlock_terminal stdout fmt ; raise error
end
- else
+ else
Pretty_utils.nullprintf text
let pp_all_warn_categories_status () =
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 9fd4675ec6b..89936f3185b 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -45,17 +45,17 @@ type 'a pretty_printer =
(**
Generic type for the various logging channels which are not aborting
Frama-C.
- - When [current] is [false] (default for most of the channels),
- no location is output. When it is [true], the last registered location
- is used as current (see {!Cil_const.CurrentLoc}).
+ - When [current] is [false] (default for most of the channels),
+ no location is output. When it is [true], the last registered location
+ is used as current (see {!Cil_const.CurrentLoc}).
- [source] is the location to be output. If nil, [current] is used to
- determine if a location should be output
+ determine if a location should be output
- [emitwith] function which is called each time an event is processed
- [echo] is [true] if the event should be output somewhere in addition
- to [stdout]
+ to [stdout]
- [append] adds some actions performed on the formatter after the event
- has been processed.
- @since Beryllium-20090601-beta1 *)
+ has been processed.
+ @since Beryllium-20090601-beta1 *)
type ('a,'b) pretty_aborter =
?current:bool -> ?source:Filepath.position -> ?echo:bool ->
@@ -120,7 +120,7 @@ module type Messages = sig
type category
(** category for debugging/verbose messages. Must be registered before
- any use.
+ any use.
Each column in the string defines a sub-category, e.g.
a:b:c defines a subcategory c of b, which is itself a subcategory of a.
Enabling a category (via -plugin-msg-category) will enable all its
@@ -140,7 +140,7 @@ module type Messages = sig
val debug_atleast : int -> bool
(** @since Beryllium-20090601-beta1 *)
- val printf : ?level:int -> ?dkey:category ->
+ val printf : ?level:int -> ?dkey:category ->
?current:bool -> ?source:Filepath.position ->
?append:(Format.formatter -> unit) ->
?header:(Format.formatter -> unit) ->
@@ -202,7 +202,7 @@ module type Messages = sig
[false].
The intended usage is: [assert (verify e "Bla...") ;].
- @since Beryllium-20090601-beta1
+ @since Beryllium-20090601-beta1
@plugin development guide *)
val not_yet_implemented : ('a,formatter,unit,'b) format4 -> 'a
@@ -242,13 +242,13 @@ module type Messages = sig
(** Generic log routine. The default kind is [Result]. Use cases (with
[n,m > 0]):
- [log ~verbose:n]: emit the message only when verbosity level is
- at least [n].
+ at least [n].
- [log ~debug:n]: emit the message only when debugging level is
- at least [n].
+ at least [n].
- [log ~verbose:n ~debug:m]: any debugging or verbosity level is
- sufficient.
- @since Beryllium-20090901
- @plugin development guide *)
+ sufficient.
+ @since Beryllium-20090901
+ @plugin development guide *)
val logwith : (event option -> 'b) ->
?wkey:warn_category -> ?emitwith:(event -> unit) -> ?once:bool ->
@@ -397,14 +397,14 @@ module Register
val set_echo : ?plugin:string -> ?kind:kind list -> bool -> unit
(** Turns echo on or off. Applies to all channel unless specified,
and all kind of messages unless specified.
- @since Beryllium-20090601-beta1
+ @since Beryllium-20090601-beta1
@plugin development guide *)
val add_listener : ?plugin:string -> ?kind:kind list -> (event -> unit) -> unit
(** Register a hook that is called each time an event is
emitted. Applies to all channel unless specified,
and all kind of messages unless specified.
- @since Beryllium-20090601-beta1
+ @since Beryllium-20090601-beta1
@plugin development guide *)
val echo : event -> unit
@@ -426,7 +426,7 @@ type channel
(** @since Beryllium-20090601-beta1 *)
val new_channel : string -> channel
-(** @since Beryllium-20090901
+(** @since Beryllium-20090901
@plugin development guide *)
val log_channel : channel ->
@@ -447,7 +447,7 @@ val kernel_label_name: string
val source : file:Filepath.Normalized.t -> line:int -> Filepath.position
(** @since Chlorine-20180501
@modify 18.0-Argon change type of [file]
- *)
+*)
val get_current_source : unit -> Filepath.position
@@ -463,7 +463,7 @@ val clean : unit -> unit
val null : formatter
[@@ deprecated "Use 'Pretty_utils.null' instead"]
(** Prints nothing.
- @since Beryllium-20090901
+ @since Beryllium-20090901
@deprecated Chlorine-20180501 use {!Pretty_utils} instead. *)
val nullprintf : ('a,formatter,unit) format -> 'a
@@ -480,7 +480,7 @@ val with_null : (unit -> 'b) -> ('a,formatter,unit,'b) format4 -> 'a
val set_output : ?isatty:bool -> (string -> int -> int -> unit) -> (unit -> unit) -> unit
(** This function has the same parameters as Format.make_formatter.
- @since Beryllium-20090901
+ @since Beryllium-20090901
@plugin development guide *)
val print_on_output : (Format.formatter -> unit) -> unit
@@ -490,8 +490,8 @@ val print_on_output : (Format.formatter -> unit) -> unit
Notification of listeners is not delayed, however.
Can not be recursively invoked.
- @since Beryllium-20090901
- @modify Nitrogen-20111001 signature changed
+ @since Beryllium-20090901
+ @modify Nitrogen-20111001 signature changed
@plugin development guide *)
val print_delayed : (Format.formatter -> unit) -> unit
@@ -502,7 +502,7 @@ val print_delayed : (Format.formatter -> unit) -> unit
Can not be recursively invoked.
@since Beryllium-20090901
- @modify Nitrogen-20111001 signature changed
+ @modify Nitrogen-20111001 signature changed
@plugin development guide *)
(**/**)
@@ -528,7 +528,7 @@ val treat_deferred_error: unit -> unit
a delayed error or failure. Currently done:
- after each command-line stage.
- after each analysis step (as separated by -then and its derivatives),
- including the last one.
+ including the last one.
*)
(**/**)
--
GitLab