From 6e6fc8e62c983400fd1f7919190f46509035515e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 12 Jul 2022 16:19:04 +0200
Subject: [PATCH] [wp] json report documented
---
src/plugins/wp/doc/manual/wp_plugin.tex | 59 +++++++++++++++++++++++--
src/plugins/wp/register.ml | 5 ++-
2 files changed, 59 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 978329a251f..361b7e2e948 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1631,11 +1631,64 @@ Reports are generated with the following command-line options:
(described below).
\item[\tt -wp-report-basename <name>] set the basename for exported
reports (described below).
-\item[\tt -wp-report-json <file>.json] output the reports in JSON format.
- If the file already exists, it is used to stabilize the \verb+range+ of steps
- reports in all other reports (see below).
+\item[\tt -wp-report-json <file>.json] output the proof report in JSON format.
\end{description}
+See sections below for details on the generated report formats.
+
+\clearpage
+\subsection{JSON Reports}
+
+The generated JSON report format consists of an array of JSON records, one for
+each generated toplevel goal. Each record consists of the following fields,
+some of them being optional when indicated:
+
+\begin{description}
+\raggedright
+\itemsep0pt
+\newcommand{\jsarray}[1]{[#1,\ldots]}
+\item[\tt "goal":<string>] goal identifier (same as in console report);
+\item[\tt "property":<string>] property identifier (see \textsf{Frama-C/Report} documentation);
+\item[\tt "file":<string>] source file location;
+\item[\tt "line":<number>] source line location;
+\item[\tt "axiomatic"?:<string>] axiomatic name (optional);
+\item[\tt "function"?:<string>] function name (optional);
+\item[\tt "behavior"?:<string>] behavior name (optional, non-default);
+\item[\tt "smoke":<boolean>] smoke-tests goal
+ (\textbf{warning:} Cf. fields \verb+"verdict"+ and \verb+"passed"+ below);
+\item[\tt "verdict":<string>] prover returned status. Can be \verb+"none"+,
+ \verb+"valid"+, \verb+"failed"+, \verb+"unknown"+, \verb+"stepout"+ or
+ \verb+"timeout"+ (\textbf{warning:} Cf. field \verb+"passed"+ below);
+\item[\tt "passed":<boolean>] is \verb+"true"+ when the prover verdict is valid for non-smoke tests,
+ or when the prover verdict is \textit{not} valid for smoke tests;
+\item[\tt "script"?:<string>] script file, when available (optional);
+\item[\tt "tactics"?:<number>] number of tactics involved in the script (optional);
+\item[\tt "provers":\jsarray{<prover>}] prover detailed output. Each entry of the array is a record
+ that consists of the following fields:
+ \begin{description}
+ \item[\tt "prover":<string>] prover name (with version, see option \texttt{-wp-prover});
+ \item[\tt "time":<number>] prover time, in milliseconds. For \texttt{Qed}
+ prover, includes also the total simplification time for other provers and
+ tactics that contributes to the goal;
+ \item[\tt "success":<number>] number of valid sub-goals the prover contributes to.
+ \end{description}
+\item[\tt "subgoals"?:<number>] number of associated sub-goals (optional, when more than one);
+\item[\tt "proved"?:<number>] number of sub-goals proved (optional, when non-zero);
+\item[\tt "failed"?:<number>] number of sub-goals ending with prover failure or failed smoke-tests
+ (optional, when non-zero);
+\item[\tt "timeout"?:<number>] number of sub-goals ending in timeout or step-out
+ (except for smoke-tests) (optional, when non-zero);
+\item[\tt "unknown"?:<number>] number of sub-goals with unknown verdict
+ (except for smoke-tests) (optional, when non-zero);
+\item[\tt "cached"?:<number>] number of cached sub-goals verdicts
+ (including \texttt{Qed} proved sub-goals) (optional, when non-zero).
+\end{description}
+
+Notice that the JSON report file is printed in compact form without extra space nor indentation,
+unless verbose level is greater than 2 or debug level is greater than 1.
+
+\subsection{Template-based Reports}
+
Reports are created from user defined wp-report specification files.
The general format of a wp-report file is as follows:
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index c30767e2dc4..05ad50660a9 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -250,6 +250,8 @@ let stats_to_json g (s : Stats.stats) : Json.t =
"function", `String (Kernel_function.get_name kf);
"behavior", `String bhv ;
] in
+ let proofs = Stats.proofs s in
+ let subgoals = if proofs > 1 then ["subgoals", `Int proofs] else [] in
`Assoc
([
"goal", `String g.po_gid ;
@@ -262,13 +264,12 @@ let stats_to_json g (s : Stats.stats) : Json.t =
"verdict", `String (VCS.name_of_verdict s.verdict) ;
] @ script @ [
"provers", `List (List.map pstats_to_json s.provers) ;
- ] @
+ ] @ subgoals @
List.filter (function (_,`Int n) -> n > 0 | _ -> true) [
"tactics", `Int s.tactics;
"proved", `Int s.proved;
"timeout", `Int s.timeout;
"unknown", `Int s.unknown ;
- "noresult", `Int s.noresult ;
"failed", `Int s.failed ;
"cached", `Int s.cached ;
])
--
GitLab