diff --git a/Makefile b/Makefile
index 8b2e0e805f772f40f62a3b545f3dafa032047b6e..647c9af39913a6426e12726286ad2892783d631b 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 4b3ef56f0a6cffb0436ecc0ac3f95556798d6d98..90d5cf66c32343299306fd0110f1b41dd815a5de 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 0000000000000000000000000000000000000000..4ca48f5aa7e65cd010e2214e31c862290fa213a0
--- /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 0000000000000000000000000000000000000000..0a4fdc2a7be73dd4f59058968d4a96b2e2ca2f47
--- /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 5e18e6c1492bb2e7be86a280efd6fb8e69d3aeff..4884c022eaee34b73c4d10a918b39da902856915 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 f92e9ad97db69f4b205b941c026b81843a8c34ce..52c7f9b91f229c7bb42338e6e1ce544bb6e97993 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 ddf1be28132cef2717a63e266d47e895fac8cb6b..e75414667ebed4235e8818a972a98ec77200749e 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 3f4ab94f35323b73bda4e9933cdf48fd3afc665e..b247313aab64aee2dc88d21cd76fd681667f62d8 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} *)
(* ************************************************************************* *)