From 68cf30ea609f40981350d7ef061acaac8f13cc3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 25 Feb 2019 10:46:34 +0100
Subject: [PATCH] [wp] differenciate report-in and report-out for json
---
src/plugins/wp/register.ml | 19 ++++++++++++++-----
src/plugins/wp/wpReport.ml | 19 ++++++++++++++-----
src/plugins/wp/wpReport.mli | 2 +-
3 files changed, 29 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index b8bbb65f08b..1eeeeedbfb6 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -139,13 +139,22 @@ let do_wp_print_for goals =
let do_wp_report () =
begin
- let rfiles = Wp_parameters.Report.get () in
- if rfiles <> [] then
+ let reports = Wp_parameters.Report.get () in
+ let jreport = Wp_parameters.ReportJson.get () in
+ if reports <> [] || jreport <> "" then
begin
let stats = WpReport.fcstat () in
- let jfile = Wp_parameters.ReportJson.get () in
- if jfile <> "" then WpReport.export_json stats jfile ;
- List.iter (WpReport.export stats) rfiles ;
+ begin
+ match Transitioning.String.split_on_char ':' jreport with
+ | [] | [""] -> ()
+ | [joutput] ->
+ WpReport.export_json stats ~joutput () ;
+ | [jinput;joutput] ->
+ WpReport.export_json stats ~jinput ~joutput () ;
+ | _ ->
+ Wp_parameters.error "Invalid format for option -wp-report-json"
+ end ;
+ List.iter (WpReport.export stats) reports ;
end ;
if Wp_parameters.MemoryContext.get () then
wp_warn_memory_context ()
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index a14264c93f0..6b319bb4fa5 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -864,20 +864,29 @@ let export gstat specfile =
(* -------------------------------------------------------------------------- *)
-let export_json gstat jfile =
+let export_json gstat ?jinput ~joutput () =
begin
- Wp_parameters.feedback "Report '%s'" jfile ;
let js =
try
- if Sys.file_exists jfile
- then Json.load_file jfile else `Null
+ let jfile = match jinput with
+ | None ->
+ Wp_parameters.feedback "Report '%s'" joutput ;
+ joutput
+ | Some jinput ->
+ Wp_parameters.feedback "Report in: '%s'" jinput ;
+ Wp_parameters.feedback "Report out: '%s'" joutput ;
+ jinput
+ in
+ if Sys.file_exists jfile then
+ Json.load_file jfile
+ else `Null
with Json.Error(file,line,msg) ->
let source = Log.source ~file ~line in
Wp_parameters.error ~source "Incorrect json file: %s" msg ;
`Null
in
rankify_fcstat gstat js ;
- Json.save_file jfile (json_of_fcstat gstat) ;
+ Json.save_file joutput (json_of_fcstat gstat) ;
end
diff --git a/src/plugins/wp/wpReport.mli b/src/plugins/wp/wpReport.mli
index 6d3563ff35c..01b4c67af6a 100644
--- a/src/plugins/wp/wpReport.mli
+++ b/src/plugins/wp/wpReport.mli
@@ -47,4 +47,4 @@ type fcstat
val fcstat : unit -> fcstat
val export : fcstat -> string -> unit
-val export_json : fcstat -> string -> unit
+val export_json : fcstat -> ?jinput:string -> joutput:string -> unit -> unit
--
GitLab