From 2532b96a61ca31c221a16d59c645e6530d87caf9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 13 Feb 2018 19:57:27 +0100
Subject: [PATCH] [kernel] Better API for message keys
- Debug_category is now only used for its side-effects, the only
relevant state is in Log.messages
- allow to use `String.split_on_char` in `Transitioning`
---
.gitignore | 1 +
Makefile | 7 +++++-
configure.in | 7 ++++++
headers/header_spec.txt | 2 +-
share/Makefile.config.in | 4 +++
.../plugin_entry_points/log.ml | 12 ++-------
.../plugin_entry_points/plugin.ml | 25 ++++++-------------
.../plugin_entry_points/plugin.mli | 9 ++++---
.../{transitioning.ml => transitioning.ml.in} | 16 ++++++++++++
src/libraries/stdlib/transitioning.mli | 1 +
src/plugins/pdg/register.ml | 9 +++++--
src/plugins/wp/register.ml | 10 ++++++--
tests/misc/oracle/my_visitor.res.oracle | 4 +--
tests/saveload/oracle/basic.4.res.oracle | 2 +-
14 files changed, 69 insertions(+), 40 deletions(-)
rename src/libraries/stdlib/{transitioning.ml => transitioning.ml.in} (88%)
diff --git a/.gitignore b/.gitignore
index e04ec9e2d72..a05dad8ccf4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -188,3 +188,4 @@ hello-*.tar.gz
#######################
# should remain empty #
#######################
+/src/libraries/stdlib/transitioning.ml
diff --git a/Makefile b/Makefile
index 5893fde2a10..746a5d2d232 100644
--- a/Makefile
+++ b/Makefile
@@ -397,7 +397,12 @@ LIB_CMO =\
src/libraries/utils/filepath \
src/libraries/utils/json
-GENERATED+= src/libraries/utils/json.ml
+GENERATED+= src/libraries/utils/json.ml src/libraries/stdlib/transitioning.ml
+
+src/libraries/stdlib/transitioning.ml: src/libraries/stdlib/transitioning.ml.in
+ rm -f $@
+ sed -e 's/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g' $< > $@
+ $(CHMOD_RO) $@
NON_OPAQUE_DEPS+=\
src/libraries/datatype/unmarshal_z \
diff --git a/configure.in b/configure.in
index 40f7e2abc41..1fe68d89da7 100644
--- a/configure.in
+++ b/configure.in
@@ -113,6 +113,13 @@ case $OCAMLVERSION in
OCAML_ANNOT_OPTION="-bin-annot";;
esac
+AC_SUBST(SPLIT_ON_CHAR)
+
+case $OCAMLVERSION in
+ 4.02.*|4.03.*) SPLIT_ON_CHAR=split_on_char;;
+ *) SPLIT_ON_CHAR=String.split_on_char;;
+esac
+
# Ocaml library path
AC_MSG_CHECKING(OCaml library path)
OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 376bf399edf..a5524a27481 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -601,7 +601,7 @@ src/libraries/stdlib/extlib.ml: CEA_LGPL
src/libraries/stdlib/extlib.mli: CEA_LGPL
src/libraries/stdlib/integer.ml: CEA_LGPL
src/libraries/stdlib/integer.mli: CEA_LGPL
-src/libraries/stdlib/transitioning.ml: CEA_LGPL
+src/libraries/stdlib/transitioning.ml.in: CEA_LGPL
src/libraries/stdlib/transitioning.mli: CEA_LGPL
src/libraries/utils/README.md: .ignore
src/libraries/utils/bag.ml: CEA_LGPL
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index e932db64f96..cce395f7691 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -83,6 +83,10 @@ PTESTSBEST ?=@PTESTSBEST@
DEVELOPMENT ?=@DEVELOPMENT@
+# Compatibility across OCaml versions
+
+SPLIT_ON_CHAR ?= @SPLIT_ON_CHAR@
+
#############
# Libraries #
#############
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 617fb1f0ad1..434ef1f4549 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -705,16 +705,8 @@ struct
end
let split_category s =
- let rec aux l s =
- if String.contains s ':' then begin
- let i = String.rindex s ':' in
- let super = String.sub s 0 i in
- let sub = String.sub s (i+1) (String.length s - i - 1) in
- aux (sub::l) super
- end else s :: l
- in
- if s = "*" || s = "" then []
- else aux [] s
+ let s = if s = "*" then "" else s in
+ List.filter (fun s -> s <> "") (Transitioning.String.split_on_char ':' s)
let merge_category l =
match l with
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 2207542e67e..1c09251503b 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -39,7 +39,7 @@ module type S_no_log = sig
module Help: Parameter_sig.Bool
module Verbose: Parameter_sig.Int
module Debug: Parameter_sig.Int
- module Debug_category: Parameter_sig.String_list
+ module Debug_category: Parameter_sig.String
module Share: Parameter_sig.Specific_dir
module Session: Parameter_sig.Specific_dir
module Config: Parameter_sig.Specific_dir
@@ -618,9 +618,8 @@ struct
end
let debug_category_optname = output_mode "Msg_key" "msg-key"
- let () = Parameter_customize.no_category ()
module Debug_category =
- String_list(struct
+ Empty_string(struct
let option_name = debug_category_optname
let arg_name="k1[,...,kn]"
let help =
@@ -630,26 +629,16 @@ struct
all categories"
end)
- let rec remove_common_prefix before after =
- match before, after with
- | [], l -> l
- | hd1 :: tl1, hd2 :: tl2 ->
- if hd1 <> hd2 then begin
- L.warning "Unexpected values in debug categories update"
- end;
- remove_common_prefix tl1 tl2
- | _ :: _, [] -> L.warning "Unexpected values in debug categories update"; []
-
let () =
let is_kernel = is_kernel () in
let module D = Datatype in
Debug_category.add_set_hook
- (fun before after ->
- let changes = remove_common_prefix before after in
- if List.mem "help" changes then
+ (fun _ s ->
+ let categories = Transitioning.String.split_on_char ',' s in
+ if List.mem "help" categories then
(* level 0 just in case user ask to display all categories
in an otherwise quiet run *)
- Cmdline.run_after_exiting_stage
+ Cmdline.run_after_exiting_stage
(fun () -> L.pp_all_categories (); raise Cmdline.Exit)
else
let add_or_del flag c () =
@@ -673,7 +662,7 @@ struct
end else add_or_del to_add c ()
end
in
- List.iter action changes)
+ List.iter action categories)
let () = reset_plugin ()
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 9c9f0e030ef..8f96759274d 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -42,11 +42,14 @@ module type S_no_log = sig
module Verbose: Parameter_sig.Int
module Debug: Parameter_sig.Int
- module Debug_category: Parameter_sig.String_list
- (** prints debug messages having the corresponding key.
+ module Debug_category: Parameter_sig.String
+ (** prints debug messages having the corresponding key. Note that
+ the actual value of the parameter is irrelevant. What is important is
+ what is stored in the corresponding Log.Messages instantiation
+ (see {!Plugin.S} below).
@since Oxygen-20120901
@modify Fluorine-20130401 Set instead of list
- @modify Frama-C+dev List instead of String
+ @modify Frama-C+dev String instead of Set
*)
(** Handle the specific `share' directory of the plug-in.
diff --git a/src/libraries/stdlib/transitioning.ml b/src/libraries/stdlib/transitioning.ml.in
similarity index 88%
rename from src/libraries/stdlib/transitioning.ml
rename to src/libraries/stdlib/transitioning.ml.in
index f151ccc2dcc..9632ab32e77 100644
--- a/src/libraries/stdlib/transitioning.ml
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -20,6 +20,21 @@
(* *)
(**************************************************************************)
+let split_on_char c s =
+ let rec aux res s =
+ if String.contains s c then begin
+ let i = String.rindex s c in
+ let prefix = String.sub s 0 i in
+ let suf = String.sub s (i+1) (String.length s - i - 1) in
+ aux (suf::res) prefix
+ end else s :: res
+ in
+ aux [] s
+
+(* the implementation above is only used in case we compile against an
+ old OCaml version. Avoid unused warning in other cases. *)
+let _ = split_on_char
+
[@@@ warning "-3"]
module String = struct
@@ -27,6 +42,7 @@ module String = struct
let capitalize_ascii = String.capitalize
let uncapitalize_ascii = String.uncapitalize
let lowercase_ascii = String.lowercase
+ let split_on_char = @SPLIT_ON_CHAR@
end
module Char = struct
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 99e1bb3803e..2a528b5381c 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -43,6 +43,7 @@ module String: sig
val capitalize_ascii: string -> string
val uncapitalize_ascii: string -> string
val lowercase_ascii: string -> string
+ val split_on_char: char -> string -> string list
end
(** See above documentation for [String] *)
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 56e5287f6f4..c5d1401d703 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -137,8 +137,13 @@ let compute () =
!Db.Pdg.extract pdg (dot_basename ^ "." ^ fname ^ ".dot")
in
Callgraph.Uses.iter_in_rev_order do_kf_pdg;
- Pdg_parameters.debug "Logging keys : %s"
- (Pdg_parameters.Debug_category.As_string.get ());
+ let pp_sep fmt () = Format.pp_print_string fmt "," in
+ let pp_cat fmt (cat:Pdg_parameters.category) =
+ Format.pp_print_string fmt (cat:>string)
+ in
+ Pdg_parameters.debug "Logging keys : %a"
+ (Format.pp_print_list ~pp_sep pp_cat)
+ (Pdg_parameters.get_debug_keys ());
if Pdg_parameters.BuildAll.get () then
Pdg_parameters.feedback "====== PDG GRAPH COMPUTED ======"
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 2d0b12c16fe..7a8f165d67f 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -849,9 +849,15 @@ let sequence jobs () =
else try_sequence jobs ()
let tracelog () =
- if Wp_parameters.Debug_category.is_empty () then
+ let active_keys = Wp_parameters.get_debug_keys () in
+ if active_keys <> [] then begin
+ let pp_sep fmt () = Format.pp_print_string fmt "," in
+ let pp_cat fmt (cat:Wp_parameters.category) =
+ Format.pp_print_string fmt (cat:>string)
+ in
Wp_parameters.debug
- "Logging keys: %s." (Wp_parameters.Debug_category.As_string.get ())
+ "Logging keys: %a." Format.(pp_print_list ~pp_sep pp_cat) active_keys
+ end
let main = sequence [
(fun () -> Wp_parameters.debug ~dkey:job_key "Start WP plugin...@.") ;
diff --git a/tests/misc/oracle/my_visitor.res.oracle b/tests/misc/oracle/my_visitor.res.oracle
index dcdcd2818c9..2b68d647f3b 100644
--- a/tests/misc/oracle/my_visitor.res.oracle
+++ b/tests/misc/oracle/my_visitor.res.oracle
@@ -1,9 +1,9 @@
[kernel] warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] warning: 14 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] warning: 14 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */
int f(void)
diff --git a/tests/saveload/oracle/basic.4.res.oracle b/tests/saveload/oracle/basic.4.res.oracle
index 7ad320b638d..ddb7afcc1da 100644
--- a/tests/saveload/oracle/basic.4.res.oracle
+++ b/tests/saveload/oracle/basic.4.res.oracle
@@ -1,2 +1,2 @@
-[kernel] warning: 12 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] warning: 11 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: ignoring source files specified on the command line while loading a global initial context.
--
GitLab