From ace2ca068cd53660a6514ecfa04f6880d09feaca Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 27 Jul 2023 13:42:26 +0200
Subject: [PATCH] [wp/ivette] update API
---
src/plugins/wp/wpApi.ml | 5 ++---
src/plugins/wp/wpTipApi.ml | 2 +-
2 files changed, 3 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 56a72d3c7c9..3fc1548fc16 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -117,7 +117,7 @@ struct
"total", Jnumber;
])
let to_json (smoke,cs) : Json.t =
- let verdict = match cs.Stats.verdict with
+ let verdict = match cs.Stats.best with
| VCS.Valid -> if smoke then "Doomed" else "Valid"
| VCS.Unknown -> if smoke then "Passed" else "Unknown"
| Failed -> "Failure"
@@ -125,7 +125,6 @@ struct
| Computing _ -> "Computing"
| Timeout -> "Timeout"
| Stepout -> "Stepout"
- | Invalid -> "Invalid"
in
let summary = Format.asprintf "%s%a" verdict
(Stats.pp_stats ~shell:false ~cache:Update) cs
@@ -133,7 +132,7 @@ struct
"summary", `String summary ;
"tactics", `Int cs.tactics ;
"proved", `Int cs.proved ;
- "total", `Int (Stats.proofs cs) ;
+ "total", `Int (Stats.subgoals cs) ;
]
end
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index ce27c6b39a5..2bceb850f99 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -64,7 +64,7 @@ let () =
set_proved rq (ProofEngine.proved node) ;
set_pending rq (ProofEngine.pending node) ;
let s = ProofEngine.stats node in
- set_size rq (Stats.proofs s) ;
+ set_size rq (Stats.subgoals s) ;
set_stats rq (Pretty_utils.to_string Stats.pretty s) ;
end
--
GitLab