From 6e91fa9505ea52b4c0838a9e85a7868aa230d2fa Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 2 Sep 2019 16:06:59 +0200
Subject: [PATCH] [kernel] add an option to dump the current configuration into
a Json object
---
Makefile | 1 +
headers/header_spec.txt | 2 +
src/kernel_internals/runtime/dump_config.ml | 66 +++++++++++++++++++
src/kernel_internals/runtime/dump_config.mli | 24 +++++++
src/kernel_services/ast_queries/file.ml | 3 +
src/kernel_services/ast_queries/file.mli | 6 ++
.../plugin_entry_points/kernel.ml | 11 ++++
.../plugin_entry_points/kernel.mli | 4 ++
8 files changed, 117 insertions(+)
create mode 100644 src/kernel_internals/runtime/dump_config.ml
create mode 100644 src/kernel_internals/runtime/dump_config.mli
diff --git a/Makefile b/Makefile
index 8b2e0e805f7..647c9af3991 100644
--- a/Makefile
+++ b/Makefile
@@ -627,6 +627,7 @@ KERNEL_CMO=\
src/kernel_services/ast_transformations/clone.cmo \
src/kernel_services/ast_transformations/filter.cmo \
src/kernel_services/ast_transformations/inline.cmo \
+ src/kernel_internals/runtime/dump_config.cmo \
src/kernel_internals/runtime/special_hooks.cmo \
src/kernel_internals/runtime/messages.cmo
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 4b3ef56f0a6..90d5cf66c32 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -367,6 +367,8 @@ src/kernel_internals/parsing/logic_preprocess.mli: CEA_INRIA_LGPL
src/kernel_internals/parsing/logic_preprocess.mll: CEA_INRIA_LGPL
src/kernel_internals/runtime/README.md: .ignore
src/kernel_internals/runtime/boot.ml: CEA_LGPL
+src/kernel_internals/runtime/dump_config.ml: CEA_LGPL
+src/kernel_internals/runtime/dump_config.mli: CEA_LGPL
src/kernel_internals/runtime/fc_config.ml.in: CEA_LGPL
src/kernel_internals/runtime/fc_config.mli: CEA_LGPL
src/kernel_internals/runtime/frama_c_config.ml.in: CEA_LGPL
diff --git a/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml
new file mode 100644
index 00000000000..4ca48f5aa7e
--- /dev/null
+++ b/src/kernel_internals/runtime/dump_config.ml
@@ -0,0 +1,66 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let dump_to_stdout () =
+ let string s = `String s in
+ let list f l = `List (List.map f l) in
+ let json = `Assoc [
+ "version", `String Fc_config.version ;
+ "codename", `String Fc_config.codename ;
+ "version_and_codename", `String Fc_config.version_and_codename ;
+ "major_version", `Int Fc_config.major_version ;
+ "minor_version", `Int Fc_config.minor_version ;
+ "is_gui", `Bool !Fc_config.is_gui ;
+ "ocamlc", `String Fc_config.ocamlc ;
+ "ocamlopt", `String Fc_config.ocamlopt ;
+ "ocaml_wflags", `String Fc_config.ocaml_wflags ;
+ "datadir", `String Fc_config.datadir ;
+ "datadirs", list string Fc_config.datadirs ;
+ "framac_libc", `String Fc_config.framac_libc ;
+ "libdir", `String Fc_config.libdir ;
+ "plugin_dir", list string Fc_config.plugin_dir ;
+ "plugin_path", `String Fc_config.plugin_path ;
+ "compilation_unit_names", list string Fc_config.compilation_unit_names ;
+ "library_names", list string Fc_config.library_names ;
+ "preprocessor", `String Fc_config.preprocessor ;
+ "using_default_cpp", `Bool Fc_config.using_default_cpp ;
+ "preprocessor_is_gnu_like", `Bool Fc_config.preprocessor_is_gnu_like ;
+ "preprocessor_supported_arch_options",
+ list string Fc_config.preprocessor_supported_arch_options ;
+ "preprocessor_keep_comments", `Bool Fc_config.preprocessor_keep_comments ;
+ "dot", (match Fc_config.dot with Some cmd -> `String cmd | None -> `Null) ;
+ "current_machdep", `String (Kernel.Machdep.get ()) ;
+ "machdeps", list string (File.list_available_machdeps ())
+ ]
+ in
+ Yojson.Basic.pretty_to_channel stdout json
+
+let () =
+ let action () =
+ if Kernel.DumpConfig.get () then begin
+ dump_to_stdout ();
+ raise Cmdline.Exit
+ end else
+ Cmdline.nop
+ in
+ Cmdline.run_after_exiting_stage action
+
diff --git a/src/kernel_internals/runtime/dump_config.mli b/src/kernel_internals/runtime/dump_config.mli
new file mode 100644
index 00000000000..0a4fdc2a7be
--- /dev/null
+++ b/src/kernel_internals/runtime/dump_config.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+val dump_to_stdout : unit -> unit
+(** Dumps a Json object describing the Frama-C configuration *)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 5e18e6c1492..4884c022eae 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -396,6 +396,9 @@ let get_machdep () =
with Not_found -> (* Should not happen given the checks above *)
Kernel.fatal "Machdep %s not registered" m
+let list_available_machdeps () =
+ Machdeps.fold (fun m _ acc -> m :: acc) (List.map fst default_machdeps)
+
let pretty_machdep ?fmt ?machdep () =
let machine = match machdep with None -> get_machdep () | Some m -> m in
match fmt with
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index f92e9ad97db..52c7f9b91f2 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -69,6 +69,12 @@ val machdep_macro: string -> string
@since Magnesium-20151001 (exported in the API)
*)
+val list_available_machdeps: unit -> string list
+(** [list_available_machdeps ()] gives the list of the names of available
+ machdeps, starting with the ones added with new_machdep and ending with
+ the list of default machdeps.
+ @since Frama-C+dev *)
+
type code_transformation_category
(** type of registered code transformations
@since Neon-20140301
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index ddf1be28132..e75414667eb 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -418,6 +418,17 @@ let () =
if not (DumpDependencies.is_default ()) then
State_dependency_graph.dump (DumpDependencies.get ()))
+let () = Parameter_customize.set_group help
+let () = Parameter_customize.set_cmdline_stage Cmdline.Exiting
+module DumpConfig =
+ False
+ (struct
+ let module_name = "DumpConfig"
+ let option_name = "-dump-config"
+ let help = "dump several information about frama-configuration inside \
+ JSON object"
+ end)
+
let () = Parameter_customize.set_group help
let () = Parameter_customize.set_cmdline_stage Cmdline.Exiting
let () = Parameter_customize.do_not_journalize ()
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 3f4ab94f353..b247313aab6 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -238,6 +238,10 @@ module PrintPluginPath: Parameter_sig.Bool
module AutocompleteHelp: Parameter_sig.String_set
(** Behavior of option "-autocomplete" *)
+module DumpConfig: Parameter_sig.Bool
+(** Behavior of option "-dump-config"
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Output Messages} *)
(* ************************************************************************* *)
--
GitLab