From e1e3cdb2f2834efbfba6b40eb46adc17f7734be3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 7 Oct 2020 17:36:06 +0200
Subject: [PATCH] [Kernel] add documentation for option -print-config-json
---
doc/userman/user-changes.tex | 2 ++
doc/userman/user-start.tex | 4 ++++
man/frama-c.1 | 5 ++++-
man/frama-c.1.header | 2 +-
man/frama-c.1.md | 3 +++
src/kernel_internals/runtime/dump_config.ml | 1 +
src/kernel_internals/runtime/dump_config.mli | 4 ++--
src/kernel_services/plugin_entry_points/kernel.ml | 4 ++--
8 files changed, 19 insertions(+), 6 deletions(-)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 625dcc2db4a..c2d12813685 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 ef3dd8f71b3..ca5e3138665 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/man/frama-c.1 b/man/frama-c.1
index 92ee3debed2..f175412be20 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 8d12fafa546..c70585242be 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 30c76c5d3c5..ca5a103976c 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/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml
index a6f89a5e9f5..15ffcdaad28 100644
--- a/src/kernel_internals/runtime/dump_config.ml
+++ b/src/kernel_internals/runtime/dump_config.ml
@@ -51,6 +51,7 @@ let dump_to_json () =
"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 ;
diff --git a/src/kernel_internals/runtime/dump_config.mli b/src/kernel_internals/runtime/dump_config.mli
index ea08b4981ee..018f6f72255 100644
--- a/src/kernel_internals/runtime/dump_config.mli
+++ b/src/kernel_internals/runtime/dump_config.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
val dump_to_json : unit -> Yojson.Basic.t
-(** Builds a Json object describing the Frama-C configuration *)
+(** Builds a Json object describing the Frama-C configuration. *)
val dump_to_stdout : unit -> unit
-(** Dumps a Json object to describing the Frama-C configuration to stdout *)
+(** Dumps a Json object describing the Frama-C configuration to stdout. *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 5663b635e02..b95618a9b88 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -425,8 +425,8 @@ module PrintConfigJson =
(struct
let module_name = "PrintConfigJson"
let option_name = "-print-config-json"
- let help = "print several information about frama-configuration inside a \
- JSON object"
+ let help = "prints extensive data about Frama-C's configuration, in \
+ JSON format, and exits."
end)
let () = Parameter_customize.set_group help
--
GitLab