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/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 625dcc2db4a5fcfaa313c0d255f070bfd3b320b5..c2d128136851bdda4d32c1a012e7dd380691b341 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -6,6 +6,8 @@ release. First we list changes of the last release.
\section*{\nextframacversion}
\begin{itemize}
+\item \textbf{Getting Started:} added option
+ \texttt{-print-config-json}.
\item \textbf{Getting Started:} added option
\texttt{-autocomplete}.
\item \textbf{Getting Started:} updated installation instructions.
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index ef3dd8f71b3110428d896da94b838e8cc0aa2ac5..ca5e31386653aaea9e25f0834e63a5bdc0503401 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -146,6 +146,10 @@ all documented with \texttt{-kernel-h}:
There are many aliases for these options, but for backward compatibility purposes only.
Those listed above should be used for scripting.
+For a more thorough display of configuration-related data, in JSON format,
+use option \optiondef{-}{print-config-json}. Note that the data output by this
+option is likely to change in future releases.
+
\subsection{Options Outline}
The batch and interactive versions of \FramaC obey a number of
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/man/frama-c.1 b/man/frama-c.1
index 92ee3debed2a8a3d2436bfb37cebe1338704a786..f175412be20b91f5b8c7a1d557822d8e9831fa3d 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -25,7 +25,7 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2020-09-21
+.TH FRAMA-C 1 2020-10-07
.SH NAME
.PP
frama-c[.byte] - a static analyzer for C programs
@@ -437,6 +437,9 @@ Defaults to no.
.B -print-cpp-commands
outputs the preprocessing commands for all input files.
.TP
+.B -print-config-json
+outputs extensive Frama-C configuration data in JSON format.
+.TP
.B [-no]-print-libc
expands \f[B]#include\f[R] directives in the pretty-printed CIL code for
files in the Frama-C standard library.
diff --git a/man/frama-c.1.header b/man/frama-c.1.header
index 8d12fafa546d1e339543e2998e30ae71d8248f46..c70585242be9b04d9332047bf305dd8626f45879 100644
--- a/man/frama-c.1.header
+++ b/man/frama-c.1.header
@@ -25,4 +25,4 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2020-09-21
+.TH FRAMA-C 1 2020-10-07
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 30c76c5d3c59430a1b1abd0ea0661a02d708e008..ca5a103976ccf8734e9140b313d240ca0c79cac4 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -340,6 +340,9 @@ See also **-cpp-frama-c-compliant**.
-print-cpp-commands
: outputs the preprocessing commands for all input files.
+-print-config-json
+: outputs extensive Frama-C configuration data in JSON format.
+
[-no]-print-libc
: expands **#include** directives in the pretty-printed CIL code for files in
the Frama-C standard library. Defaults to no.
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index 33819b87e89f0f0b109c67d441dc2ce4c94faf75..1ec1be6c901fd44c3129614bbebfb3c12adfd42e 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -31,6 +31,7 @@ import re
import shutil
import shlex
import glob
+import json
from subprocess import Popen, PIPE
from pathlib import Path
import function_finder
@@ -72,27 +73,16 @@ if "PTESTS_TESTING" in os.environ:
fc_stubs_c.touch()
gnumakefile.touch()
-process = Popen([framac_bin / "frama-c", "-no-autoload-plugins", "-print-share-path"], stdout=PIPE)
+process = Popen([framac_bin / "frama-c", "-print-config-json"], stdout=PIPE)
(output, err) = process.communicate()
-output = output.decode('utf-8')
exit_code = process.wait()
if exit_code != 0:
sys.exit(f"error running frama-c -print-share-path")
-sharedir = Path(output)
-
-def get_known_machdeps():
- process = Popen([framac_bin / "frama-c", "-machdep", "help"], stdout=PIPE)
- (output, err) = process.communicate()
- output = output.decode('utf-8')
- exit_code = process.wait()
- if exit_code != 0:
- sys.exit("error getting machdeps: " + output)
- match = re.match("\[kernel\] supported machines are (.*) \(default is (.*)\).", output, re.DOTALL)
- if not match:
- sys.exit("error getting known machdeps: " + output)
- machdeps = match.group(1).split()
- default_machdep = match.group(2)
- return (default_machdep, machdeps)
+
+fc_config = json.loads(output.decode('utf-8'))
+sharedir = Path(fc_config['datadir'])
+default_machdep = fc_config['current_machdep']
+machdeps = fc_config['machdeps']
def check_path_exists(path):
if path.exists():
@@ -172,7 +162,6 @@ if yn != "" and (yn[0] == "Y" or yn[0] == "y"):
add_main_stub = True
print("Please define the architectural model (machdep) of the target machine.")
-(default_machdep, machdeps) = get_known_machdeps()
print("Known machdeps: " + " ".join(machdeps))
machdep_chosen = False
while not machdep_chosen:
diff --git a/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml
new file mode 100644
index 0000000000000000000000000000000000000000..15ffcdaad28cd58a3006b69de9b954946abec2ac
--- /dev/null
+++ b/src/kernel_internals/runtime/dump_config.ml
@@ -0,0 +1,91 @@
+(**************************************************************************)
+(* *)
+(* 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 list_plugin_names () =
+ Plugin.fold_on_plugins (fun p acc -> p.Plugin.p_name :: acc) []
+
+let dump_parameter tp =
+ let open Typed_parameter in
+ let json_value = match tp.accessor with
+ | Bool (accessor,_) -> `Bool (accessor.get ())
+ | Int (accessor,_) -> `Int (accessor.get ())
+ | String (accessor,_) -> `String (accessor.get ())
+ in
+ tp.name, json_value
+
+let dump_all_parameters () =
+ let add_category _ l acc =
+ List.fold_left (fun acc tp -> dump_parameter tp :: acc) acc l
+ in
+ let add_plugin plugin acc =
+ Hashtbl.fold add_category plugin.Plugin.p_parameters acc
+ in
+ Plugin.fold_on_plugins add_plugin []
+
+let dump_to_json () =
+ let string s = `String s in
+ let list f l = `List (List.map f l) in
+ `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 ;
+ "lablgtk", `String Fc_config.lablgtk ;
+ "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 ()) ;
+ "plugins", list string (list_plugin_names ()) ;
+ "parameters", `Assoc (dump_all_parameters ()) ;
+ ]
+
+let dump_to_stdout () =
+ let json = dump_to_json () in
+ Yojson.Basic.(pretty_to_channel stdout (sort json))
+
+let () =
+ let action () =
+ if Kernel.PrintConfigJson.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..018f6f72255b3fe3ce065072b18903c578405fcb
--- /dev/null
+++ b/src/kernel_internals/runtime/dump_config.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* 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_json : unit -> Yojson.Basic.t
+(** Builds a Json object describing the Frama-C configuration. *)
+
+val dump_to_stdout : unit -> unit
+(** Dumps a Json object describing the Frama-C configuration to stdout. *)
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..0ddeab5c75a42c32227c2d5099582104a5a112c4 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -418,6 +418,18 @@ 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 PrintConfigJson =
+ False
+ (struct
+ let module_name = "PrintConfigJson"
+ let option_name = "-print-config-json"
+ let help = "prints extensive data about Frama-C's configuration, in \
+ JSON format, and exits (experimental: the output format \
+ is very likely to change in future versions)."
+ 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..c81f3efefe7163adf572bb7ff3f34d0f35e8d635 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 PrintConfigJson: Parameter_sig.Bool
+(** Behavior of option "-print-config-json"
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Output Messages} *)
(* ************************************************************************* *)